0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 486 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 91 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 568 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇔, 29 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇒, 0 ms)
↳27 QDP
↳28 QDPSizeChangeProof (⇔, 0 ms)
↳29 YES
addK_in_aag(b, b, b) → addK_out_aag(b, b, b)
addK_in_aag(zero(T69), b, zero(T69)) → U34_aag(T69, binaryZA_in_g(T69))
binaryZA_in_g(zero(T75)) → U1_g(T75, binaryZA_in_g(T75))
binaryZA_in_g(one(T79)) → U2_g(T79, binaryB_in_g(T79))
binaryB_in_g(b) → binaryB_out_g(b)
binaryB_in_g(zero(T84)) → U3_g(T84, binaryZA_in_g(T84))
U3_g(T84, binaryZA_out_g(T84)) → binaryB_out_g(zero(T84))
binaryB_in_g(one(T88)) → U4_g(T88, binaryB_in_g(T88))
U4_g(T88, binaryB_out_g(T88)) → binaryB_out_g(one(T88))
U2_g(T79, binaryB_out_g(T79)) → binaryZA_out_g(one(T79))
U1_g(T75, binaryZA_out_g(T75)) → binaryZA_out_g(zero(T75))
U34_aag(T69, binaryZA_out_g(T69)) → addK_out_aag(zero(T69), b, zero(T69))
addK_in_aag(one(T93), b, one(T93)) → U35_aag(T93, binaryB_in_g(T93))
U35_aag(T93, binaryB_out_g(T93)) → addK_out_aag(one(T93), b, one(T93))
addK_in_aag(b, T98, T98) → U36_aag(T98, binaryZA_in_g(T98))
U36_aag(T98, binaryZA_out_g(T98)) → addK_out_aag(b, T98, T98)
addK_in_aag(T114, T115, T113) → U37_aag(T114, T115, T113, addzJ_in_aag(T114, T115, T113))
addzJ_in_aag(zero(T134), zero(T135), zero(T133)) → U30_aag(T134, T135, T133, addzC_in_aag(T134, T135, T133))
addzC_in_aag(zero(T154), zero(T155), zero(T153)) → U5_aag(T154, T155, T153, addzC_in_aag(T154, T155, T153))
addzC_in_aag(zero(T174), one(T175), one(T173)) → U6_aag(T174, T175, T173, addxD_in_aag(T174, T175, T173))
addxD_in_aag(one(T181), b, one(T181)) → U24_aag(T181, binaryB_in_g(T181))
U24_aag(T181, binaryB_out_g(T181)) → addxD_out_aag(one(T181), b, one(T181))
addxD_in_aag(zero(T186), b, zero(T186)) → U25_aag(T186, binaryZA_in_g(T186))
U25_aag(T186, binaryZA_out_g(T186)) → addxD_out_aag(zero(T186), b, zero(T186))
addxD_in_aag(T202, T203, T201) → U26_aag(T202, T203, T201, addzC_in_aag(T202, T203, T201))
addzC_in_aag(one(T222), zero(T223), one(T221)) → U7_aag(T222, T223, T221, addyE_in_aag(T222, T223, T221))
addyE_in_aag(b, one(T229), one(T229)) → U27_aag(T229, binaryB_in_g(T229))
U27_aag(T229, binaryB_out_g(T229)) → addyE_out_aag(b, one(T229), one(T229))
addyE_in_aag(b, zero(T234), zero(T234)) → U28_aag(T234, binaryZA_in_g(T234))
U28_aag(T234, binaryZA_out_g(T234)) → addyE_out_aag(b, zero(T234), zero(T234))
addyE_in_aag(T250, T251, T249) → U29_aag(T250, T251, T249, addzC_in_aag(T250, T251, T249))
addzC_in_aag(one(T264), one(T265), zero(T263)) → U8_aag(T264, T265, T263, addcF_in_aag(T264, T265, T263))
addcF_in_aag(b, b, one(b)) → addcF_out_aag(b, b, one(b))
addcF_in_aag(T276, b, T275) → U21_aag(T276, T275, succZH_in_ag(T276, T275))
succZH_in_ag(zero(T282), one(T282)) → U11_ag(T282, binaryZA_in_g(T282))
U11_ag(T282, binaryZA_out_g(T282)) → succZH_out_ag(zero(T282), one(T282))
succZH_in_ag(one(T290), zero(T289)) → U12_ag(T290, T289, succG_in_ag(T290, T289))
succG_in_ag(b, one(b)) → succG_out_ag(b, one(b))
succG_in_ag(zero(T295), one(T295)) → U9_ag(T295, binaryZA_in_g(T295))
U9_ag(T295, binaryZA_out_g(T295)) → succG_out_ag(zero(T295), one(T295))
succG_in_ag(one(T303), zero(T302)) → U10_ag(T303, T302, succG_in_ag(T303, T302))
U10_ag(T303, T302, succG_out_ag(T303, T302)) → succG_out_ag(one(T303), zero(T302))
U12_ag(T290, T289, succG_out_ag(T290, T289)) → succZH_out_ag(one(T290), zero(T289))
U21_aag(T276, T275, succZH_out_ag(T276, T275)) → addcF_out_aag(T276, b, T275)
addcF_in_aag(b, T314, T313) → U22_aag(T314, T313, succZH_in_ag(T314, T313))
U22_aag(T314, T313, succZH_out_ag(T314, T313)) → addcF_out_aag(b, T314, T313)
addcF_in_aag(T330, T331, T329) → U23_aag(T330, T331, T329, addCI_in_aag(T330, T331, T329))
addCI_in_aag(zero(T350), zero(T351), one(T349)) → U13_aag(T350, T351, T349, addzC_in_aag(T350, T351, T349))
U13_aag(T350, T351, T349, addzC_out_aag(T350, T351, T349)) → addCI_out_aag(zero(T350), zero(T351), one(T349))
addCI_in_aag(zero(zero(T377)), one(b), zero(one(T377))) → U14_aag(T377, binaryZA_in_g(T377))
U14_aag(T377, binaryZA_out_g(T377)) → addCI_out_aag(zero(zero(T377)), one(b), zero(one(T377)))
addCI_in_aag(zero(one(T389)), one(b), zero(zero(T388))) → U15_aag(T389, T388, succG_in_ag(T389, T388))
U15_aag(T389, T388, succG_out_ag(T389, T388)) → addCI_out_aag(zero(one(T389)), one(b), zero(zero(T388)))
addCI_in_aag(zero(T404), one(T405), zero(T403)) → U16_aag(T404, T405, T403, addCI_in_aag(T404, T405, T403))
addCI_in_aag(one(b), zero(zero(T431)), zero(one(T431))) → U17_aag(T431, binaryZA_in_g(T431))
U17_aag(T431, binaryZA_out_g(T431)) → addCI_out_aag(one(b), zero(zero(T431)), zero(one(T431)))
addCI_in_aag(one(b), zero(one(T443)), zero(zero(T442))) → U18_aag(T443, T442, succG_in_ag(T443, T442))
U18_aag(T443, T442, succG_out_ag(T443, T442)) → addCI_out_aag(one(b), zero(one(T443)), zero(zero(T442)))
addCI_in_aag(one(T458), zero(T459), zero(T457)) → U19_aag(T458, T459, T457, addCI_in_aag(T458, T459, T457))
addCI_in_aag(one(T472), one(T473), one(T471)) → U20_aag(T472, T473, T471, addcF_in_aag(T472, T473, T471))
U20_aag(T472, T473, T471, addcF_out_aag(T472, T473, T471)) → addCI_out_aag(one(T472), one(T473), one(T471))
U19_aag(T458, T459, T457, addCI_out_aag(T458, T459, T457)) → addCI_out_aag(one(T458), zero(T459), zero(T457))
U16_aag(T404, T405, T403, addCI_out_aag(T404, T405, T403)) → addCI_out_aag(zero(T404), one(T405), zero(T403))
U23_aag(T330, T331, T329, addCI_out_aag(T330, T331, T329)) → addcF_out_aag(T330, T331, T329)
U8_aag(T264, T265, T263, addcF_out_aag(T264, T265, T263)) → addzC_out_aag(one(T264), one(T265), zero(T263))
U29_aag(T250, T251, T249, addzC_out_aag(T250, T251, T249)) → addyE_out_aag(T250, T251, T249)
U7_aag(T222, T223, T221, addyE_out_aag(T222, T223, T221)) → addzC_out_aag(one(T222), zero(T223), one(T221))
U26_aag(T202, T203, T201, addzC_out_aag(T202, T203, T201)) → addxD_out_aag(T202, T203, T201)
U6_aag(T174, T175, T173, addxD_out_aag(T174, T175, T173)) → addzC_out_aag(zero(T174), one(T175), one(T173))
U5_aag(T154, T155, T153, addzC_out_aag(T154, T155, T153)) → addzC_out_aag(zero(T154), zero(T155), zero(T153))
U30_aag(T134, T135, T133, addzC_out_aag(T134, T135, T133)) → addzJ_out_aag(zero(T134), zero(T135), zero(T133))
addzJ_in_aag(zero(T489), one(T490), one(T488)) → U31_aag(T489, T490, T488, addxD_in_aag(T489, T490, T488))
U31_aag(T489, T490, T488, addxD_out_aag(T489, T490, T488)) → addzJ_out_aag(zero(T489), one(T490), one(T488))
addzJ_in_aag(one(T507), zero(T508), one(T506)) → U32_aag(T507, T508, T506, addyE_in_aag(T507, T508, T506))
U32_aag(T507, T508, T506, addyE_out_aag(T507, T508, T506)) → addzJ_out_aag(one(T507), zero(T508), one(T506))
addzJ_in_aag(one(T519), one(T520), zero(T518)) → U33_aag(T519, T520, T518, addcF_in_aag(T519, T520, T518))
U33_aag(T519, T520, T518, addcF_out_aag(T519, T520, T518)) → addzJ_out_aag(one(T519), one(T520), zero(T518))
U37_aag(T114, T115, T113, addzJ_out_aag(T114, T115, T113)) → addK_out_aag(T114, T115, T113)
addK_in_aag(b, zero(T527), zero(T527)) → U38_aag(T527, binaryZA_in_g(T527))
U38_aag(T527, binaryZA_out_g(T527)) → addK_out_aag(b, zero(T527), zero(T527))
addK_in_aag(b, one(T533), one(T533)) → U39_aag(T533, binaryB_in_g(T533))
U39_aag(T533, binaryB_out_g(T533)) → addK_out_aag(b, one(T533), one(T533))
addK_in_aag(T548, T549, T547) → U40_aag(T548, T549, T547, addzJ_in_aag(T548, T549, T547))
U40_aag(T548, T549, T547, addzJ_out_aag(T548, T549, T547)) → addK_out_aag(T548, T549, T547)
addK_in_aag(zero(T576), zero(T577), zero(T575)) → U41_aag(T576, T577, T575, addzC_in_aag(T576, T577, T575))
U41_aag(T576, T577, T575, addzC_out_aag(T576, T577, T575)) → addK_out_aag(zero(T576), zero(T577), zero(T575))
addK_in_aag(zero(T596), one(T597), one(T595)) → U42_aag(T596, T597, T595, addxD_in_aag(T596, T597, T595))
U42_aag(T596, T597, T595, addxD_out_aag(T596, T597, T595)) → addK_out_aag(zero(T596), one(T597), one(T595))
addK_in_aag(one(T614), zero(T615), one(T613)) → U43_aag(T614, T615, T613, addyE_in_aag(T614, T615, T613))
U43_aag(T614, T615, T613, addyE_out_aag(T614, T615, T613)) → addK_out_aag(one(T614), zero(T615), one(T613))
addK_in_aag(one(T626), one(T627), zero(T625)) → U44_aag(T626, T627, T625, addcF_in_aag(T626, T627, T625))
U44_aag(T626, T627, T625, addcF_out_aag(T626, T627, T625)) → addK_out_aag(one(T626), one(T627), zero(T625))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
addK_in_aag(b, b, b) → addK_out_aag(b, b, b)
addK_in_aag(zero(T69), b, zero(T69)) → U34_aag(T69, binaryZA_in_g(T69))
binaryZA_in_g(zero(T75)) → U1_g(T75, binaryZA_in_g(T75))
binaryZA_in_g(one(T79)) → U2_g(T79, binaryB_in_g(T79))
binaryB_in_g(b) → binaryB_out_g(b)
binaryB_in_g(zero(T84)) → U3_g(T84, binaryZA_in_g(T84))
U3_g(T84, binaryZA_out_g(T84)) → binaryB_out_g(zero(T84))
binaryB_in_g(one(T88)) → U4_g(T88, binaryB_in_g(T88))
U4_g(T88, binaryB_out_g(T88)) → binaryB_out_g(one(T88))
U2_g(T79, binaryB_out_g(T79)) → binaryZA_out_g(one(T79))
U1_g(T75, binaryZA_out_g(T75)) → binaryZA_out_g(zero(T75))
U34_aag(T69, binaryZA_out_g(T69)) → addK_out_aag(zero(T69), b, zero(T69))
addK_in_aag(one(T93), b, one(T93)) → U35_aag(T93, binaryB_in_g(T93))
U35_aag(T93, binaryB_out_g(T93)) → addK_out_aag(one(T93), b, one(T93))
addK_in_aag(b, T98, T98) → U36_aag(T98, binaryZA_in_g(T98))
U36_aag(T98, binaryZA_out_g(T98)) → addK_out_aag(b, T98, T98)
addK_in_aag(T114, T115, T113) → U37_aag(T114, T115, T113, addzJ_in_aag(T114, T115, T113))
addzJ_in_aag(zero(T134), zero(T135), zero(T133)) → U30_aag(T134, T135, T133, addzC_in_aag(T134, T135, T133))
addzC_in_aag(zero(T154), zero(T155), zero(T153)) → U5_aag(T154, T155, T153, addzC_in_aag(T154, T155, T153))
addzC_in_aag(zero(T174), one(T175), one(T173)) → U6_aag(T174, T175, T173, addxD_in_aag(T174, T175, T173))
addxD_in_aag(one(T181), b, one(T181)) → U24_aag(T181, binaryB_in_g(T181))
U24_aag(T181, binaryB_out_g(T181)) → addxD_out_aag(one(T181), b, one(T181))
addxD_in_aag(zero(T186), b, zero(T186)) → U25_aag(T186, binaryZA_in_g(T186))
U25_aag(T186, binaryZA_out_g(T186)) → addxD_out_aag(zero(T186), b, zero(T186))
addxD_in_aag(T202, T203, T201) → U26_aag(T202, T203, T201, addzC_in_aag(T202, T203, T201))
addzC_in_aag(one(T222), zero(T223), one(T221)) → U7_aag(T222, T223, T221, addyE_in_aag(T222, T223, T221))
addyE_in_aag(b, one(T229), one(T229)) → U27_aag(T229, binaryB_in_g(T229))
U27_aag(T229, binaryB_out_g(T229)) → addyE_out_aag(b, one(T229), one(T229))
addyE_in_aag(b, zero(T234), zero(T234)) → U28_aag(T234, binaryZA_in_g(T234))
U28_aag(T234, binaryZA_out_g(T234)) → addyE_out_aag(b, zero(T234), zero(T234))
addyE_in_aag(T250, T251, T249) → U29_aag(T250, T251, T249, addzC_in_aag(T250, T251, T249))
addzC_in_aag(one(T264), one(T265), zero(T263)) → U8_aag(T264, T265, T263, addcF_in_aag(T264, T265, T263))
addcF_in_aag(b, b, one(b)) → addcF_out_aag(b, b, one(b))
addcF_in_aag(T276, b, T275) → U21_aag(T276, T275, succZH_in_ag(T276, T275))
succZH_in_ag(zero(T282), one(T282)) → U11_ag(T282, binaryZA_in_g(T282))
U11_ag(T282, binaryZA_out_g(T282)) → succZH_out_ag(zero(T282), one(T282))
succZH_in_ag(one(T290), zero(T289)) → U12_ag(T290, T289, succG_in_ag(T290, T289))
succG_in_ag(b, one(b)) → succG_out_ag(b, one(b))
succG_in_ag(zero(T295), one(T295)) → U9_ag(T295, binaryZA_in_g(T295))
U9_ag(T295, binaryZA_out_g(T295)) → succG_out_ag(zero(T295), one(T295))
succG_in_ag(one(T303), zero(T302)) → U10_ag(T303, T302, succG_in_ag(T303, T302))
U10_ag(T303, T302, succG_out_ag(T303, T302)) → succG_out_ag(one(T303), zero(T302))
U12_ag(T290, T289, succG_out_ag(T290, T289)) → succZH_out_ag(one(T290), zero(T289))
U21_aag(T276, T275, succZH_out_ag(T276, T275)) → addcF_out_aag(T276, b, T275)
addcF_in_aag(b, T314, T313) → U22_aag(T314, T313, succZH_in_ag(T314, T313))
U22_aag(T314, T313, succZH_out_ag(T314, T313)) → addcF_out_aag(b, T314, T313)
addcF_in_aag(T330, T331, T329) → U23_aag(T330, T331, T329, addCI_in_aag(T330, T331, T329))
addCI_in_aag(zero(T350), zero(T351), one(T349)) → U13_aag(T350, T351, T349, addzC_in_aag(T350, T351, T349))
U13_aag(T350, T351, T349, addzC_out_aag(T350, T351, T349)) → addCI_out_aag(zero(T350), zero(T351), one(T349))
addCI_in_aag(zero(zero(T377)), one(b), zero(one(T377))) → U14_aag(T377, binaryZA_in_g(T377))
U14_aag(T377, binaryZA_out_g(T377)) → addCI_out_aag(zero(zero(T377)), one(b), zero(one(T377)))
addCI_in_aag(zero(one(T389)), one(b), zero(zero(T388))) → U15_aag(T389, T388, succG_in_ag(T389, T388))
U15_aag(T389, T388, succG_out_ag(T389, T388)) → addCI_out_aag(zero(one(T389)), one(b), zero(zero(T388)))
addCI_in_aag(zero(T404), one(T405), zero(T403)) → U16_aag(T404, T405, T403, addCI_in_aag(T404, T405, T403))
addCI_in_aag(one(b), zero(zero(T431)), zero(one(T431))) → U17_aag(T431, binaryZA_in_g(T431))
U17_aag(T431, binaryZA_out_g(T431)) → addCI_out_aag(one(b), zero(zero(T431)), zero(one(T431)))
addCI_in_aag(one(b), zero(one(T443)), zero(zero(T442))) → U18_aag(T443, T442, succG_in_ag(T443, T442))
U18_aag(T443, T442, succG_out_ag(T443, T442)) → addCI_out_aag(one(b), zero(one(T443)), zero(zero(T442)))
addCI_in_aag(one(T458), zero(T459), zero(T457)) → U19_aag(T458, T459, T457, addCI_in_aag(T458, T459, T457))
addCI_in_aag(one(T472), one(T473), one(T471)) → U20_aag(T472, T473, T471, addcF_in_aag(T472, T473, T471))
U20_aag(T472, T473, T471, addcF_out_aag(T472, T473, T471)) → addCI_out_aag(one(T472), one(T473), one(T471))
U19_aag(T458, T459, T457, addCI_out_aag(T458, T459, T457)) → addCI_out_aag(one(T458), zero(T459), zero(T457))
U16_aag(T404, T405, T403, addCI_out_aag(T404, T405, T403)) → addCI_out_aag(zero(T404), one(T405), zero(T403))
U23_aag(T330, T331, T329, addCI_out_aag(T330, T331, T329)) → addcF_out_aag(T330, T331, T329)
U8_aag(T264, T265, T263, addcF_out_aag(T264, T265, T263)) → addzC_out_aag(one(T264), one(T265), zero(T263))
U29_aag(T250, T251, T249, addzC_out_aag(T250, T251, T249)) → addyE_out_aag(T250, T251, T249)
U7_aag(T222, T223, T221, addyE_out_aag(T222, T223, T221)) → addzC_out_aag(one(T222), zero(T223), one(T221))
U26_aag(T202, T203, T201, addzC_out_aag(T202, T203, T201)) → addxD_out_aag(T202, T203, T201)
U6_aag(T174, T175, T173, addxD_out_aag(T174, T175, T173)) → addzC_out_aag(zero(T174), one(T175), one(T173))
U5_aag(T154, T155, T153, addzC_out_aag(T154, T155, T153)) → addzC_out_aag(zero(T154), zero(T155), zero(T153))
U30_aag(T134, T135, T133, addzC_out_aag(T134, T135, T133)) → addzJ_out_aag(zero(T134), zero(T135), zero(T133))
addzJ_in_aag(zero(T489), one(T490), one(T488)) → U31_aag(T489, T490, T488, addxD_in_aag(T489, T490, T488))
U31_aag(T489, T490, T488, addxD_out_aag(T489, T490, T488)) → addzJ_out_aag(zero(T489), one(T490), one(T488))
addzJ_in_aag(one(T507), zero(T508), one(T506)) → U32_aag(T507, T508, T506, addyE_in_aag(T507, T508, T506))
U32_aag(T507, T508, T506, addyE_out_aag(T507, T508, T506)) → addzJ_out_aag(one(T507), zero(T508), one(T506))
addzJ_in_aag(one(T519), one(T520), zero(T518)) → U33_aag(T519, T520, T518, addcF_in_aag(T519, T520, T518))
U33_aag(T519, T520, T518, addcF_out_aag(T519, T520, T518)) → addzJ_out_aag(one(T519), one(T520), zero(T518))
U37_aag(T114, T115, T113, addzJ_out_aag(T114, T115, T113)) → addK_out_aag(T114, T115, T113)
addK_in_aag(b, zero(T527), zero(T527)) → U38_aag(T527, binaryZA_in_g(T527))
U38_aag(T527, binaryZA_out_g(T527)) → addK_out_aag(b, zero(T527), zero(T527))
addK_in_aag(b, one(T533), one(T533)) → U39_aag(T533, binaryB_in_g(T533))
U39_aag(T533, binaryB_out_g(T533)) → addK_out_aag(b, one(T533), one(T533))
addK_in_aag(T548, T549, T547) → U40_aag(T548, T549, T547, addzJ_in_aag(T548, T549, T547))
U40_aag(T548, T549, T547, addzJ_out_aag(T548, T549, T547)) → addK_out_aag(T548, T549, T547)
addK_in_aag(zero(T576), zero(T577), zero(T575)) → U41_aag(T576, T577, T575, addzC_in_aag(T576, T577, T575))
U41_aag(T576, T577, T575, addzC_out_aag(T576, T577, T575)) → addK_out_aag(zero(T576), zero(T577), zero(T575))
addK_in_aag(zero(T596), one(T597), one(T595)) → U42_aag(T596, T597, T595, addxD_in_aag(T596, T597, T595))
U42_aag(T596, T597, T595, addxD_out_aag(T596, T597, T595)) → addK_out_aag(zero(T596), one(T597), one(T595))
addK_in_aag(one(T614), zero(T615), one(T613)) → U43_aag(T614, T615, T613, addyE_in_aag(T614, T615, T613))
U43_aag(T614, T615, T613, addyE_out_aag(T614, T615, T613)) → addK_out_aag(one(T614), zero(T615), one(T613))
addK_in_aag(one(T626), one(T627), zero(T625)) → U44_aag(T626, T627, T625, addcF_in_aag(T626, T627, T625))
U44_aag(T626, T627, T625, addcF_out_aag(T626, T627, T625)) → addK_out_aag(one(T626), one(T627), zero(T625))
ADDK_IN_AAG(zero(T69), b, zero(T69)) → U34_AAG(T69, binaryZA_in_g(T69))
ADDK_IN_AAG(zero(T69), b, zero(T69)) → BINARYZA_IN_G(T69)
BINARYZA_IN_G(zero(T75)) → U1_G(T75, binaryZA_in_g(T75))
BINARYZA_IN_G(zero(T75)) → BINARYZA_IN_G(T75)
BINARYZA_IN_G(one(T79)) → U2_G(T79, binaryB_in_g(T79))
BINARYZA_IN_G(one(T79)) → BINARYB_IN_G(T79)
BINARYB_IN_G(zero(T84)) → U3_G(T84, binaryZA_in_g(T84))
BINARYB_IN_G(zero(T84)) → BINARYZA_IN_G(T84)
BINARYB_IN_G(one(T88)) → U4_G(T88, binaryB_in_g(T88))
BINARYB_IN_G(one(T88)) → BINARYB_IN_G(T88)
ADDK_IN_AAG(one(T93), b, one(T93)) → U35_AAG(T93, binaryB_in_g(T93))
ADDK_IN_AAG(one(T93), b, one(T93)) → BINARYB_IN_G(T93)
ADDK_IN_AAG(b, T98, T98) → U36_AAG(T98, binaryZA_in_g(T98))
ADDK_IN_AAG(b, T98, T98) → BINARYZA_IN_G(T98)
ADDK_IN_AAG(T114, T115, T113) → U37_AAG(T114, T115, T113, addzJ_in_aag(T114, T115, T113))
ADDK_IN_AAG(T114, T115, T113) → ADDZJ_IN_AAG(T114, T115, T113)
ADDZJ_IN_AAG(zero(T134), zero(T135), zero(T133)) → U30_AAG(T134, T135, T133, addzC_in_aag(T134, T135, T133))
ADDZJ_IN_AAG(zero(T134), zero(T135), zero(T133)) → ADDZC_IN_AAG(T134, T135, T133)
ADDZC_IN_AAG(zero(T154), zero(T155), zero(T153)) → U5_AAG(T154, T155, T153, addzC_in_aag(T154, T155, T153))
ADDZC_IN_AAG(zero(T154), zero(T155), zero(T153)) → ADDZC_IN_AAG(T154, T155, T153)
ADDZC_IN_AAG(zero(T174), one(T175), one(T173)) → U6_AAG(T174, T175, T173, addxD_in_aag(T174, T175, T173))
ADDZC_IN_AAG(zero(T174), one(T175), one(T173)) → ADDXD_IN_AAG(T174, T175, T173)
ADDXD_IN_AAG(one(T181), b, one(T181)) → U24_AAG(T181, binaryB_in_g(T181))
ADDXD_IN_AAG(one(T181), b, one(T181)) → BINARYB_IN_G(T181)
ADDXD_IN_AAG(zero(T186), b, zero(T186)) → U25_AAG(T186, binaryZA_in_g(T186))
ADDXD_IN_AAG(zero(T186), b, zero(T186)) → BINARYZA_IN_G(T186)
ADDXD_IN_AAG(T202, T203, T201) → U26_AAG(T202, T203, T201, addzC_in_aag(T202, T203, T201))
ADDXD_IN_AAG(T202, T203, T201) → ADDZC_IN_AAG(T202, T203, T201)
ADDZC_IN_AAG(one(T222), zero(T223), one(T221)) → U7_AAG(T222, T223, T221, addyE_in_aag(T222, T223, T221))
ADDZC_IN_AAG(one(T222), zero(T223), one(T221)) → ADDYE_IN_AAG(T222, T223, T221)
ADDYE_IN_AAG(b, one(T229), one(T229)) → U27_AAG(T229, binaryB_in_g(T229))
ADDYE_IN_AAG(b, one(T229), one(T229)) → BINARYB_IN_G(T229)
ADDYE_IN_AAG(b, zero(T234), zero(T234)) → U28_AAG(T234, binaryZA_in_g(T234))
ADDYE_IN_AAG(b, zero(T234), zero(T234)) → BINARYZA_IN_G(T234)
ADDYE_IN_AAG(T250, T251, T249) → U29_AAG(T250, T251, T249, addzC_in_aag(T250, T251, T249))
ADDYE_IN_AAG(T250, T251, T249) → ADDZC_IN_AAG(T250, T251, T249)
ADDZC_IN_AAG(one(T264), one(T265), zero(T263)) → U8_AAG(T264, T265, T263, addcF_in_aag(T264, T265, T263))
ADDZC_IN_AAG(one(T264), one(T265), zero(T263)) → ADDCF_IN_AAG(T264, T265, T263)
ADDCF_IN_AAG(T276, b, T275) → U21_AAG(T276, T275, succZH_in_ag(T276, T275))
ADDCF_IN_AAG(T276, b, T275) → SUCCZH_IN_AG(T276, T275)
SUCCZH_IN_AG(zero(T282), one(T282)) → U11_AG(T282, binaryZA_in_g(T282))
SUCCZH_IN_AG(zero(T282), one(T282)) → BINARYZA_IN_G(T282)
SUCCZH_IN_AG(one(T290), zero(T289)) → U12_AG(T290, T289, succG_in_ag(T290, T289))
SUCCZH_IN_AG(one(T290), zero(T289)) → SUCCG_IN_AG(T290, T289)
SUCCG_IN_AG(zero(T295), one(T295)) → U9_AG(T295, binaryZA_in_g(T295))
SUCCG_IN_AG(zero(T295), one(T295)) → BINARYZA_IN_G(T295)
SUCCG_IN_AG(one(T303), zero(T302)) → U10_AG(T303, T302, succG_in_ag(T303, T302))
SUCCG_IN_AG(one(T303), zero(T302)) → SUCCG_IN_AG(T303, T302)
ADDCF_IN_AAG(b, T314, T313) → U22_AAG(T314, T313, succZH_in_ag(T314, T313))
ADDCF_IN_AAG(b, T314, T313) → SUCCZH_IN_AG(T314, T313)
ADDCF_IN_AAG(T330, T331, T329) → U23_AAG(T330, T331, T329, addCI_in_aag(T330, T331, T329))
ADDCF_IN_AAG(T330, T331, T329) → ADDCI_IN_AAG(T330, T331, T329)
ADDCI_IN_AAG(zero(T350), zero(T351), one(T349)) → U13_AAG(T350, T351, T349, addzC_in_aag(T350, T351, T349))
ADDCI_IN_AAG(zero(T350), zero(T351), one(T349)) → ADDZC_IN_AAG(T350, T351, T349)
ADDCI_IN_AAG(zero(zero(T377)), one(b), zero(one(T377))) → U14_AAG(T377, binaryZA_in_g(T377))
ADDCI_IN_AAG(zero(zero(T377)), one(b), zero(one(T377))) → BINARYZA_IN_G(T377)
ADDCI_IN_AAG(zero(one(T389)), one(b), zero(zero(T388))) → U15_AAG(T389, T388, succG_in_ag(T389, T388))
ADDCI_IN_AAG(zero(one(T389)), one(b), zero(zero(T388))) → SUCCG_IN_AG(T389, T388)
ADDCI_IN_AAG(zero(T404), one(T405), zero(T403)) → U16_AAG(T404, T405, T403, addCI_in_aag(T404, T405, T403))
ADDCI_IN_AAG(zero(T404), one(T405), zero(T403)) → ADDCI_IN_AAG(T404, T405, T403)
ADDCI_IN_AAG(one(b), zero(zero(T431)), zero(one(T431))) → U17_AAG(T431, binaryZA_in_g(T431))
ADDCI_IN_AAG(one(b), zero(zero(T431)), zero(one(T431))) → BINARYZA_IN_G(T431)
ADDCI_IN_AAG(one(b), zero(one(T443)), zero(zero(T442))) → U18_AAG(T443, T442, succG_in_ag(T443, T442))
ADDCI_IN_AAG(one(b), zero(one(T443)), zero(zero(T442))) → SUCCG_IN_AG(T443, T442)
ADDCI_IN_AAG(one(T458), zero(T459), zero(T457)) → U19_AAG(T458, T459, T457, addCI_in_aag(T458, T459, T457))
ADDCI_IN_AAG(one(T458), zero(T459), zero(T457)) → ADDCI_IN_AAG(T458, T459, T457)
ADDCI_IN_AAG(one(T472), one(T473), one(T471)) → U20_AAG(T472, T473, T471, addcF_in_aag(T472, T473, T471))
ADDCI_IN_AAG(one(T472), one(T473), one(T471)) → ADDCF_IN_AAG(T472, T473, T471)
ADDZJ_IN_AAG(zero(T489), one(T490), one(T488)) → U31_AAG(T489, T490, T488, addxD_in_aag(T489, T490, T488))
ADDZJ_IN_AAG(zero(T489), one(T490), one(T488)) → ADDXD_IN_AAG(T489, T490, T488)
ADDZJ_IN_AAG(one(T507), zero(T508), one(T506)) → U32_AAG(T507, T508, T506, addyE_in_aag(T507, T508, T506))
ADDZJ_IN_AAG(one(T507), zero(T508), one(T506)) → ADDYE_IN_AAG(T507, T508, T506)
ADDZJ_IN_AAG(one(T519), one(T520), zero(T518)) → U33_AAG(T519, T520, T518, addcF_in_aag(T519, T520, T518))
ADDZJ_IN_AAG(one(T519), one(T520), zero(T518)) → ADDCF_IN_AAG(T519, T520, T518)
ADDK_IN_AAG(b, zero(T527), zero(T527)) → U38_AAG(T527, binaryZA_in_g(T527))
ADDK_IN_AAG(b, zero(T527), zero(T527)) → BINARYZA_IN_G(T527)
ADDK_IN_AAG(b, one(T533), one(T533)) → U39_AAG(T533, binaryB_in_g(T533))
ADDK_IN_AAG(b, one(T533), one(T533)) → BINARYB_IN_G(T533)
ADDK_IN_AAG(T548, T549, T547) → U40_AAG(T548, T549, T547, addzJ_in_aag(T548, T549, T547))
ADDK_IN_AAG(zero(T576), zero(T577), zero(T575)) → U41_AAG(T576, T577, T575, addzC_in_aag(T576, T577, T575))
ADDK_IN_AAG(zero(T576), zero(T577), zero(T575)) → ADDZC_IN_AAG(T576, T577, T575)
ADDK_IN_AAG(zero(T596), one(T597), one(T595)) → U42_AAG(T596, T597, T595, addxD_in_aag(T596, T597, T595))
ADDK_IN_AAG(zero(T596), one(T597), one(T595)) → ADDXD_IN_AAG(T596, T597, T595)
ADDK_IN_AAG(one(T614), zero(T615), one(T613)) → U43_AAG(T614, T615, T613, addyE_in_aag(T614, T615, T613))
ADDK_IN_AAG(one(T614), zero(T615), one(T613)) → ADDYE_IN_AAG(T614, T615, T613)
ADDK_IN_AAG(one(T626), one(T627), zero(T625)) → U44_AAG(T626, T627, T625, addcF_in_aag(T626, T627, T625))
ADDK_IN_AAG(one(T626), one(T627), zero(T625)) → ADDCF_IN_AAG(T626, T627, T625)
addK_in_aag(b, b, b) → addK_out_aag(b, b, b)
addK_in_aag(zero(T69), b, zero(T69)) → U34_aag(T69, binaryZA_in_g(T69))
binaryZA_in_g(zero(T75)) → U1_g(T75, binaryZA_in_g(T75))
binaryZA_in_g(one(T79)) → U2_g(T79, binaryB_in_g(T79))
binaryB_in_g(b) → binaryB_out_g(b)
binaryB_in_g(zero(T84)) → U3_g(T84, binaryZA_in_g(T84))
U3_g(T84, binaryZA_out_g(T84)) → binaryB_out_g(zero(T84))
binaryB_in_g(one(T88)) → U4_g(T88, binaryB_in_g(T88))
U4_g(T88, binaryB_out_g(T88)) → binaryB_out_g(one(T88))
U2_g(T79, binaryB_out_g(T79)) → binaryZA_out_g(one(T79))
U1_g(T75, binaryZA_out_g(T75)) → binaryZA_out_g(zero(T75))
U34_aag(T69, binaryZA_out_g(T69)) → addK_out_aag(zero(T69), b, zero(T69))
addK_in_aag(one(T93), b, one(T93)) → U35_aag(T93, binaryB_in_g(T93))
U35_aag(T93, binaryB_out_g(T93)) → addK_out_aag(one(T93), b, one(T93))
addK_in_aag(b, T98, T98) → U36_aag(T98, binaryZA_in_g(T98))
U36_aag(T98, binaryZA_out_g(T98)) → addK_out_aag(b, T98, T98)
addK_in_aag(T114, T115, T113) → U37_aag(T114, T115, T113, addzJ_in_aag(T114, T115, T113))
addzJ_in_aag(zero(T134), zero(T135), zero(T133)) → U30_aag(T134, T135, T133, addzC_in_aag(T134, T135, T133))
addzC_in_aag(zero(T154), zero(T155), zero(T153)) → U5_aag(T154, T155, T153, addzC_in_aag(T154, T155, T153))
addzC_in_aag(zero(T174), one(T175), one(T173)) → U6_aag(T174, T175, T173, addxD_in_aag(T174, T175, T173))
addxD_in_aag(one(T181), b, one(T181)) → U24_aag(T181, binaryB_in_g(T181))
U24_aag(T181, binaryB_out_g(T181)) → addxD_out_aag(one(T181), b, one(T181))
addxD_in_aag(zero(T186), b, zero(T186)) → U25_aag(T186, binaryZA_in_g(T186))
U25_aag(T186, binaryZA_out_g(T186)) → addxD_out_aag(zero(T186), b, zero(T186))
addxD_in_aag(T202, T203, T201) → U26_aag(T202, T203, T201, addzC_in_aag(T202, T203, T201))
addzC_in_aag(one(T222), zero(T223), one(T221)) → U7_aag(T222, T223, T221, addyE_in_aag(T222, T223, T221))
addyE_in_aag(b, one(T229), one(T229)) → U27_aag(T229, binaryB_in_g(T229))
U27_aag(T229, binaryB_out_g(T229)) → addyE_out_aag(b, one(T229), one(T229))
addyE_in_aag(b, zero(T234), zero(T234)) → U28_aag(T234, binaryZA_in_g(T234))
U28_aag(T234, binaryZA_out_g(T234)) → addyE_out_aag(b, zero(T234), zero(T234))
addyE_in_aag(T250, T251, T249) → U29_aag(T250, T251, T249, addzC_in_aag(T250, T251, T249))
addzC_in_aag(one(T264), one(T265), zero(T263)) → U8_aag(T264, T265, T263, addcF_in_aag(T264, T265, T263))
addcF_in_aag(b, b, one(b)) → addcF_out_aag(b, b, one(b))
addcF_in_aag(T276, b, T275) → U21_aag(T276, T275, succZH_in_ag(T276, T275))
succZH_in_ag(zero(T282), one(T282)) → U11_ag(T282, binaryZA_in_g(T282))
U11_ag(T282, binaryZA_out_g(T282)) → succZH_out_ag(zero(T282), one(T282))
succZH_in_ag(one(T290), zero(T289)) → U12_ag(T290, T289, succG_in_ag(T290, T289))
succG_in_ag(b, one(b)) → succG_out_ag(b, one(b))
succG_in_ag(zero(T295), one(T295)) → U9_ag(T295, binaryZA_in_g(T295))
U9_ag(T295, binaryZA_out_g(T295)) → succG_out_ag(zero(T295), one(T295))
succG_in_ag(one(T303), zero(T302)) → U10_ag(T303, T302, succG_in_ag(T303, T302))
U10_ag(T303, T302, succG_out_ag(T303, T302)) → succG_out_ag(one(T303), zero(T302))
U12_ag(T290, T289, succG_out_ag(T290, T289)) → succZH_out_ag(one(T290), zero(T289))
U21_aag(T276, T275, succZH_out_ag(T276, T275)) → addcF_out_aag(T276, b, T275)
addcF_in_aag(b, T314, T313) → U22_aag(T314, T313, succZH_in_ag(T314, T313))
U22_aag(T314, T313, succZH_out_ag(T314, T313)) → addcF_out_aag(b, T314, T313)
addcF_in_aag(T330, T331, T329) → U23_aag(T330, T331, T329, addCI_in_aag(T330, T331, T329))
addCI_in_aag(zero(T350), zero(T351), one(T349)) → U13_aag(T350, T351, T349, addzC_in_aag(T350, T351, T349))
U13_aag(T350, T351, T349, addzC_out_aag(T350, T351, T349)) → addCI_out_aag(zero(T350), zero(T351), one(T349))
addCI_in_aag(zero(zero(T377)), one(b), zero(one(T377))) → U14_aag(T377, binaryZA_in_g(T377))
U14_aag(T377, binaryZA_out_g(T377)) → addCI_out_aag(zero(zero(T377)), one(b), zero(one(T377)))
addCI_in_aag(zero(one(T389)), one(b), zero(zero(T388))) → U15_aag(T389, T388, succG_in_ag(T389, T388))
U15_aag(T389, T388, succG_out_ag(T389, T388)) → addCI_out_aag(zero(one(T389)), one(b), zero(zero(T388)))
addCI_in_aag(zero(T404), one(T405), zero(T403)) → U16_aag(T404, T405, T403, addCI_in_aag(T404, T405, T403))
addCI_in_aag(one(b), zero(zero(T431)), zero(one(T431))) → U17_aag(T431, binaryZA_in_g(T431))
U17_aag(T431, binaryZA_out_g(T431)) → addCI_out_aag(one(b), zero(zero(T431)), zero(one(T431)))
addCI_in_aag(one(b), zero(one(T443)), zero(zero(T442))) → U18_aag(T443, T442, succG_in_ag(T443, T442))
U18_aag(T443, T442, succG_out_ag(T443, T442)) → addCI_out_aag(one(b), zero(one(T443)), zero(zero(T442)))
addCI_in_aag(one(T458), zero(T459), zero(T457)) → U19_aag(T458, T459, T457, addCI_in_aag(T458, T459, T457))
addCI_in_aag(one(T472), one(T473), one(T471)) → U20_aag(T472, T473, T471, addcF_in_aag(T472, T473, T471))
U20_aag(T472, T473, T471, addcF_out_aag(T472, T473, T471)) → addCI_out_aag(one(T472), one(T473), one(T471))
U19_aag(T458, T459, T457, addCI_out_aag(T458, T459, T457)) → addCI_out_aag(one(T458), zero(T459), zero(T457))
U16_aag(T404, T405, T403, addCI_out_aag(T404, T405, T403)) → addCI_out_aag(zero(T404), one(T405), zero(T403))
U23_aag(T330, T331, T329, addCI_out_aag(T330, T331, T329)) → addcF_out_aag(T330, T331, T329)
U8_aag(T264, T265, T263, addcF_out_aag(T264, T265, T263)) → addzC_out_aag(one(T264), one(T265), zero(T263))
U29_aag(T250, T251, T249, addzC_out_aag(T250, T251, T249)) → addyE_out_aag(T250, T251, T249)
U7_aag(T222, T223, T221, addyE_out_aag(T222, T223, T221)) → addzC_out_aag(one(T222), zero(T223), one(T221))
U26_aag(T202, T203, T201, addzC_out_aag(T202, T203, T201)) → addxD_out_aag(T202, T203, T201)
U6_aag(T174, T175, T173, addxD_out_aag(T174, T175, T173)) → addzC_out_aag(zero(T174), one(T175), one(T173))
U5_aag(T154, T155, T153, addzC_out_aag(T154, T155, T153)) → addzC_out_aag(zero(T154), zero(T155), zero(T153))
U30_aag(T134, T135, T133, addzC_out_aag(T134, T135, T133)) → addzJ_out_aag(zero(T134), zero(T135), zero(T133))
addzJ_in_aag(zero(T489), one(T490), one(T488)) → U31_aag(T489, T490, T488, addxD_in_aag(T489, T490, T488))
U31_aag(T489, T490, T488, addxD_out_aag(T489, T490, T488)) → addzJ_out_aag(zero(T489), one(T490), one(T488))
addzJ_in_aag(one(T507), zero(T508), one(T506)) → U32_aag(T507, T508, T506, addyE_in_aag(T507, T508, T506))
U32_aag(T507, T508, T506, addyE_out_aag(T507, T508, T506)) → addzJ_out_aag(one(T507), zero(T508), one(T506))
addzJ_in_aag(one(T519), one(T520), zero(T518)) → U33_aag(T519, T520, T518, addcF_in_aag(T519, T520, T518))
U33_aag(T519, T520, T518, addcF_out_aag(T519, T520, T518)) → addzJ_out_aag(one(T519), one(T520), zero(T518))
U37_aag(T114, T115, T113, addzJ_out_aag(T114, T115, T113)) → addK_out_aag(T114, T115, T113)
addK_in_aag(b, zero(T527), zero(T527)) → U38_aag(T527, binaryZA_in_g(T527))
U38_aag(T527, binaryZA_out_g(T527)) → addK_out_aag(b, zero(T527), zero(T527))
addK_in_aag(b, one(T533), one(T533)) → U39_aag(T533, binaryB_in_g(T533))
U39_aag(T533, binaryB_out_g(T533)) → addK_out_aag(b, one(T533), one(T533))
addK_in_aag(T548, T549, T547) → U40_aag(T548, T549, T547, addzJ_in_aag(T548, T549, T547))
U40_aag(T548, T549, T547, addzJ_out_aag(T548, T549, T547)) → addK_out_aag(T548, T549, T547)
addK_in_aag(zero(T576), zero(T577), zero(T575)) → U41_aag(T576, T577, T575, addzC_in_aag(T576, T577, T575))
U41_aag(T576, T577, T575, addzC_out_aag(T576, T577, T575)) → addK_out_aag(zero(T576), zero(T577), zero(T575))
addK_in_aag(zero(T596), one(T597), one(T595)) → U42_aag(T596, T597, T595, addxD_in_aag(T596, T597, T595))
U42_aag(T596, T597, T595, addxD_out_aag(T596, T597, T595)) → addK_out_aag(zero(T596), one(T597), one(T595))
addK_in_aag(one(T614), zero(T615), one(T613)) → U43_aag(T614, T615, T613, addyE_in_aag(T614, T615, T613))
U43_aag(T614, T615, T613, addyE_out_aag(T614, T615, T613)) → addK_out_aag(one(T614), zero(T615), one(T613))
addK_in_aag(one(T626), one(T627), zero(T625)) → U44_aag(T626, T627, T625, addcF_in_aag(T626, T627, T625))
U44_aag(T626, T627, T625, addcF_out_aag(T626, T627, T625)) → addK_out_aag(one(T626), one(T627), zero(T625))
ADDK_IN_AAG(zero(T69), b, zero(T69)) → U34_AAG(T69, binaryZA_in_g(T69))
ADDK_IN_AAG(zero(T69), b, zero(T69)) → BINARYZA_IN_G(T69)
BINARYZA_IN_G(zero(T75)) → U1_G(T75, binaryZA_in_g(T75))
BINARYZA_IN_G(zero(T75)) → BINARYZA_IN_G(T75)
BINARYZA_IN_G(one(T79)) → U2_G(T79, binaryB_in_g(T79))
BINARYZA_IN_G(one(T79)) → BINARYB_IN_G(T79)
BINARYB_IN_G(zero(T84)) → U3_G(T84, binaryZA_in_g(T84))
BINARYB_IN_G(zero(T84)) → BINARYZA_IN_G(T84)
BINARYB_IN_G(one(T88)) → U4_G(T88, binaryB_in_g(T88))
BINARYB_IN_G(one(T88)) → BINARYB_IN_G(T88)
ADDK_IN_AAG(one(T93), b, one(T93)) → U35_AAG(T93, binaryB_in_g(T93))
ADDK_IN_AAG(one(T93), b, one(T93)) → BINARYB_IN_G(T93)
ADDK_IN_AAG(b, T98, T98) → U36_AAG(T98, binaryZA_in_g(T98))
ADDK_IN_AAG(b, T98, T98) → BINARYZA_IN_G(T98)
ADDK_IN_AAG(T114, T115, T113) → U37_AAG(T114, T115, T113, addzJ_in_aag(T114, T115, T113))
ADDK_IN_AAG(T114, T115, T113) → ADDZJ_IN_AAG(T114, T115, T113)
ADDZJ_IN_AAG(zero(T134), zero(T135), zero(T133)) → U30_AAG(T134, T135, T133, addzC_in_aag(T134, T135, T133))
ADDZJ_IN_AAG(zero(T134), zero(T135), zero(T133)) → ADDZC_IN_AAG(T134, T135, T133)
ADDZC_IN_AAG(zero(T154), zero(T155), zero(T153)) → U5_AAG(T154, T155, T153, addzC_in_aag(T154, T155, T153))
ADDZC_IN_AAG(zero(T154), zero(T155), zero(T153)) → ADDZC_IN_AAG(T154, T155, T153)
ADDZC_IN_AAG(zero(T174), one(T175), one(T173)) → U6_AAG(T174, T175, T173, addxD_in_aag(T174, T175, T173))
ADDZC_IN_AAG(zero(T174), one(T175), one(T173)) → ADDXD_IN_AAG(T174, T175, T173)
ADDXD_IN_AAG(one(T181), b, one(T181)) → U24_AAG(T181, binaryB_in_g(T181))
ADDXD_IN_AAG(one(T181), b, one(T181)) → BINARYB_IN_G(T181)
ADDXD_IN_AAG(zero(T186), b, zero(T186)) → U25_AAG(T186, binaryZA_in_g(T186))
ADDXD_IN_AAG(zero(T186), b, zero(T186)) → BINARYZA_IN_G(T186)
ADDXD_IN_AAG(T202, T203, T201) → U26_AAG(T202, T203, T201, addzC_in_aag(T202, T203, T201))
ADDXD_IN_AAG(T202, T203, T201) → ADDZC_IN_AAG(T202, T203, T201)
ADDZC_IN_AAG(one(T222), zero(T223), one(T221)) → U7_AAG(T222, T223, T221, addyE_in_aag(T222, T223, T221))
ADDZC_IN_AAG(one(T222), zero(T223), one(T221)) → ADDYE_IN_AAG(T222, T223, T221)
ADDYE_IN_AAG(b, one(T229), one(T229)) → U27_AAG(T229, binaryB_in_g(T229))
ADDYE_IN_AAG(b, one(T229), one(T229)) → BINARYB_IN_G(T229)
ADDYE_IN_AAG(b, zero(T234), zero(T234)) → U28_AAG(T234, binaryZA_in_g(T234))
ADDYE_IN_AAG(b, zero(T234), zero(T234)) → BINARYZA_IN_G(T234)
ADDYE_IN_AAG(T250, T251, T249) → U29_AAG(T250, T251, T249, addzC_in_aag(T250, T251, T249))
ADDYE_IN_AAG(T250, T251, T249) → ADDZC_IN_AAG(T250, T251, T249)
ADDZC_IN_AAG(one(T264), one(T265), zero(T263)) → U8_AAG(T264, T265, T263, addcF_in_aag(T264, T265, T263))
ADDZC_IN_AAG(one(T264), one(T265), zero(T263)) → ADDCF_IN_AAG(T264, T265, T263)
ADDCF_IN_AAG(T276, b, T275) → U21_AAG(T276, T275, succZH_in_ag(T276, T275))
ADDCF_IN_AAG(T276, b, T275) → SUCCZH_IN_AG(T276, T275)
SUCCZH_IN_AG(zero(T282), one(T282)) → U11_AG(T282, binaryZA_in_g(T282))
SUCCZH_IN_AG(zero(T282), one(T282)) → BINARYZA_IN_G(T282)
SUCCZH_IN_AG(one(T290), zero(T289)) → U12_AG(T290, T289, succG_in_ag(T290, T289))
SUCCZH_IN_AG(one(T290), zero(T289)) → SUCCG_IN_AG(T290, T289)
SUCCG_IN_AG(zero(T295), one(T295)) → U9_AG(T295, binaryZA_in_g(T295))
SUCCG_IN_AG(zero(T295), one(T295)) → BINARYZA_IN_G(T295)
SUCCG_IN_AG(one(T303), zero(T302)) → U10_AG(T303, T302, succG_in_ag(T303, T302))
SUCCG_IN_AG(one(T303), zero(T302)) → SUCCG_IN_AG(T303, T302)
ADDCF_IN_AAG(b, T314, T313) → U22_AAG(T314, T313, succZH_in_ag(T314, T313))
ADDCF_IN_AAG(b, T314, T313) → SUCCZH_IN_AG(T314, T313)
ADDCF_IN_AAG(T330, T331, T329) → U23_AAG(T330, T331, T329, addCI_in_aag(T330, T331, T329))
ADDCF_IN_AAG(T330, T331, T329) → ADDCI_IN_AAG(T330, T331, T329)
ADDCI_IN_AAG(zero(T350), zero(T351), one(T349)) → U13_AAG(T350, T351, T349, addzC_in_aag(T350, T351, T349))
ADDCI_IN_AAG(zero(T350), zero(T351), one(T349)) → ADDZC_IN_AAG(T350, T351, T349)
ADDCI_IN_AAG(zero(zero(T377)), one(b), zero(one(T377))) → U14_AAG(T377, binaryZA_in_g(T377))
ADDCI_IN_AAG(zero(zero(T377)), one(b), zero(one(T377))) → BINARYZA_IN_G(T377)
ADDCI_IN_AAG(zero(one(T389)), one(b), zero(zero(T388))) → U15_AAG(T389, T388, succG_in_ag(T389, T388))
ADDCI_IN_AAG(zero(one(T389)), one(b), zero(zero(T388))) → SUCCG_IN_AG(T389, T388)
ADDCI_IN_AAG(zero(T404), one(T405), zero(T403)) → U16_AAG(T404, T405, T403, addCI_in_aag(T404, T405, T403))
ADDCI_IN_AAG(zero(T404), one(T405), zero(T403)) → ADDCI_IN_AAG(T404, T405, T403)
ADDCI_IN_AAG(one(b), zero(zero(T431)), zero(one(T431))) → U17_AAG(T431, binaryZA_in_g(T431))
ADDCI_IN_AAG(one(b), zero(zero(T431)), zero(one(T431))) → BINARYZA_IN_G(T431)
ADDCI_IN_AAG(one(b), zero(one(T443)), zero(zero(T442))) → U18_AAG(T443, T442, succG_in_ag(T443, T442))
ADDCI_IN_AAG(one(b), zero(one(T443)), zero(zero(T442))) → SUCCG_IN_AG(T443, T442)
ADDCI_IN_AAG(one(T458), zero(T459), zero(T457)) → U19_AAG(T458, T459, T457, addCI_in_aag(T458, T459, T457))
ADDCI_IN_AAG(one(T458), zero(T459), zero(T457)) → ADDCI_IN_AAG(T458, T459, T457)
ADDCI_IN_AAG(one(T472), one(T473), one(T471)) → U20_AAG(T472, T473, T471, addcF_in_aag(T472, T473, T471))
ADDCI_IN_AAG(one(T472), one(T473), one(T471)) → ADDCF_IN_AAG(T472, T473, T471)
ADDZJ_IN_AAG(zero(T489), one(T490), one(T488)) → U31_AAG(T489, T490, T488, addxD_in_aag(T489, T490, T488))
ADDZJ_IN_AAG(zero(T489), one(T490), one(T488)) → ADDXD_IN_AAG(T489, T490, T488)
ADDZJ_IN_AAG(one(T507), zero(T508), one(T506)) → U32_AAG(T507, T508, T506, addyE_in_aag(T507, T508, T506))
ADDZJ_IN_AAG(one(T507), zero(T508), one(T506)) → ADDYE_IN_AAG(T507, T508, T506)
ADDZJ_IN_AAG(one(T519), one(T520), zero(T518)) → U33_AAG(T519, T520, T518, addcF_in_aag(T519, T520, T518))
ADDZJ_IN_AAG(one(T519), one(T520), zero(T518)) → ADDCF_IN_AAG(T519, T520, T518)
ADDK_IN_AAG(b, zero(T527), zero(T527)) → U38_AAG(T527, binaryZA_in_g(T527))
ADDK_IN_AAG(b, zero(T527), zero(T527)) → BINARYZA_IN_G(T527)
ADDK_IN_AAG(b, one(T533), one(T533)) → U39_AAG(T533, binaryB_in_g(T533))
ADDK_IN_AAG(b, one(T533), one(T533)) → BINARYB_IN_G(T533)
ADDK_IN_AAG(T548, T549, T547) → U40_AAG(T548, T549, T547, addzJ_in_aag(T548, T549, T547))
ADDK_IN_AAG(zero(T576), zero(T577), zero(T575)) → U41_AAG(T576, T577, T575, addzC_in_aag(T576, T577, T575))
ADDK_IN_AAG(zero(T576), zero(T577), zero(T575)) → ADDZC_IN_AAG(T576, T577, T575)
ADDK_IN_AAG(zero(T596), one(T597), one(T595)) → U42_AAG(T596, T597, T595, addxD_in_aag(T596, T597, T595))
ADDK_IN_AAG(zero(T596), one(T597), one(T595)) → ADDXD_IN_AAG(T596, T597, T595)
ADDK_IN_AAG(one(T614), zero(T615), one(T613)) → U43_AAG(T614, T615, T613, addyE_in_aag(T614, T615, T613))
ADDK_IN_AAG(one(T614), zero(T615), one(T613)) → ADDYE_IN_AAG(T614, T615, T613)
ADDK_IN_AAG(one(T626), one(T627), zero(T625)) → U44_AAG(T626, T627, T625, addcF_in_aag(T626, T627, T625))
ADDK_IN_AAG(one(T626), one(T627), zero(T625)) → ADDCF_IN_AAG(T626, T627, T625)
addK_in_aag(b, b, b) → addK_out_aag(b, b, b)
addK_in_aag(zero(T69), b, zero(T69)) → U34_aag(T69, binaryZA_in_g(T69))
binaryZA_in_g(zero(T75)) → U1_g(T75, binaryZA_in_g(T75))
binaryZA_in_g(one(T79)) → U2_g(T79, binaryB_in_g(T79))
binaryB_in_g(b) → binaryB_out_g(b)
binaryB_in_g(zero(T84)) → U3_g(T84, binaryZA_in_g(T84))
U3_g(T84, binaryZA_out_g(T84)) → binaryB_out_g(zero(T84))
binaryB_in_g(one(T88)) → U4_g(T88, binaryB_in_g(T88))
U4_g(T88, binaryB_out_g(T88)) → binaryB_out_g(one(T88))
U2_g(T79, binaryB_out_g(T79)) → binaryZA_out_g(one(T79))
U1_g(T75, binaryZA_out_g(T75)) → binaryZA_out_g(zero(T75))
U34_aag(T69, binaryZA_out_g(T69)) → addK_out_aag(zero(T69), b, zero(T69))
addK_in_aag(one(T93), b, one(T93)) → U35_aag(T93, binaryB_in_g(T93))
U35_aag(T93, binaryB_out_g(T93)) → addK_out_aag(one(T93), b, one(T93))
addK_in_aag(b, T98, T98) → U36_aag(T98, binaryZA_in_g(T98))
U36_aag(T98, binaryZA_out_g(T98)) → addK_out_aag(b, T98, T98)
addK_in_aag(T114, T115, T113) → U37_aag(T114, T115, T113, addzJ_in_aag(T114, T115, T113))
addzJ_in_aag(zero(T134), zero(T135), zero(T133)) → U30_aag(T134, T135, T133, addzC_in_aag(T134, T135, T133))
addzC_in_aag(zero(T154), zero(T155), zero(T153)) → U5_aag(T154, T155, T153, addzC_in_aag(T154, T155, T153))
addzC_in_aag(zero(T174), one(T175), one(T173)) → U6_aag(T174, T175, T173, addxD_in_aag(T174, T175, T173))
addxD_in_aag(one(T181), b, one(T181)) → U24_aag(T181, binaryB_in_g(T181))
U24_aag(T181, binaryB_out_g(T181)) → addxD_out_aag(one(T181), b, one(T181))
addxD_in_aag(zero(T186), b, zero(T186)) → U25_aag(T186, binaryZA_in_g(T186))
U25_aag(T186, binaryZA_out_g(T186)) → addxD_out_aag(zero(T186), b, zero(T186))
addxD_in_aag(T202, T203, T201) → U26_aag(T202, T203, T201, addzC_in_aag(T202, T203, T201))
addzC_in_aag(one(T222), zero(T223), one(T221)) → U7_aag(T222, T223, T221, addyE_in_aag(T222, T223, T221))
addyE_in_aag(b, one(T229), one(T229)) → U27_aag(T229, binaryB_in_g(T229))
U27_aag(T229, binaryB_out_g(T229)) → addyE_out_aag(b, one(T229), one(T229))
addyE_in_aag(b, zero(T234), zero(T234)) → U28_aag(T234, binaryZA_in_g(T234))
U28_aag(T234, binaryZA_out_g(T234)) → addyE_out_aag(b, zero(T234), zero(T234))
addyE_in_aag(T250, T251, T249) → U29_aag(T250, T251, T249, addzC_in_aag(T250, T251, T249))
addzC_in_aag(one(T264), one(T265), zero(T263)) → U8_aag(T264, T265, T263, addcF_in_aag(T264, T265, T263))
addcF_in_aag(b, b, one(b)) → addcF_out_aag(b, b, one(b))
addcF_in_aag(T276, b, T275) → U21_aag(T276, T275, succZH_in_ag(T276, T275))
succZH_in_ag(zero(T282), one(T282)) → U11_ag(T282, binaryZA_in_g(T282))
U11_ag(T282, binaryZA_out_g(T282)) → succZH_out_ag(zero(T282), one(T282))
succZH_in_ag(one(T290), zero(T289)) → U12_ag(T290, T289, succG_in_ag(T290, T289))
succG_in_ag(b, one(b)) → succG_out_ag(b, one(b))
succG_in_ag(zero(T295), one(T295)) → U9_ag(T295, binaryZA_in_g(T295))
U9_ag(T295, binaryZA_out_g(T295)) → succG_out_ag(zero(T295), one(T295))
succG_in_ag(one(T303), zero(T302)) → U10_ag(T303, T302, succG_in_ag(T303, T302))
U10_ag(T303, T302, succG_out_ag(T303, T302)) → succG_out_ag(one(T303), zero(T302))
U12_ag(T290, T289, succG_out_ag(T290, T289)) → succZH_out_ag(one(T290), zero(T289))
U21_aag(T276, T275, succZH_out_ag(T276, T275)) → addcF_out_aag(T276, b, T275)
addcF_in_aag(b, T314, T313) → U22_aag(T314, T313, succZH_in_ag(T314, T313))
U22_aag(T314, T313, succZH_out_ag(T314, T313)) → addcF_out_aag(b, T314, T313)
addcF_in_aag(T330, T331, T329) → U23_aag(T330, T331, T329, addCI_in_aag(T330, T331, T329))
addCI_in_aag(zero(T350), zero(T351), one(T349)) → U13_aag(T350, T351, T349, addzC_in_aag(T350, T351, T349))
U13_aag(T350, T351, T349, addzC_out_aag(T350, T351, T349)) → addCI_out_aag(zero(T350), zero(T351), one(T349))
addCI_in_aag(zero(zero(T377)), one(b), zero(one(T377))) → U14_aag(T377, binaryZA_in_g(T377))
U14_aag(T377, binaryZA_out_g(T377)) → addCI_out_aag(zero(zero(T377)), one(b), zero(one(T377)))
addCI_in_aag(zero(one(T389)), one(b), zero(zero(T388))) → U15_aag(T389, T388, succG_in_ag(T389, T388))
U15_aag(T389, T388, succG_out_ag(T389, T388)) → addCI_out_aag(zero(one(T389)), one(b), zero(zero(T388)))
addCI_in_aag(zero(T404), one(T405), zero(T403)) → U16_aag(T404, T405, T403, addCI_in_aag(T404, T405, T403))
addCI_in_aag(one(b), zero(zero(T431)), zero(one(T431))) → U17_aag(T431, binaryZA_in_g(T431))
U17_aag(T431, binaryZA_out_g(T431)) → addCI_out_aag(one(b), zero(zero(T431)), zero(one(T431)))
addCI_in_aag(one(b), zero(one(T443)), zero(zero(T442))) → U18_aag(T443, T442, succG_in_ag(T443, T442))
U18_aag(T443, T442, succG_out_ag(T443, T442)) → addCI_out_aag(one(b), zero(one(T443)), zero(zero(T442)))
addCI_in_aag(one(T458), zero(T459), zero(T457)) → U19_aag(T458, T459, T457, addCI_in_aag(T458, T459, T457))
addCI_in_aag(one(T472), one(T473), one(T471)) → U20_aag(T472, T473, T471, addcF_in_aag(T472, T473, T471))
U20_aag(T472, T473, T471, addcF_out_aag(T472, T473, T471)) → addCI_out_aag(one(T472), one(T473), one(T471))
U19_aag(T458, T459, T457, addCI_out_aag(T458, T459, T457)) → addCI_out_aag(one(T458), zero(T459), zero(T457))
U16_aag(T404, T405, T403, addCI_out_aag(T404, T405, T403)) → addCI_out_aag(zero(T404), one(T405), zero(T403))
U23_aag(T330, T331, T329, addCI_out_aag(T330, T331, T329)) → addcF_out_aag(T330, T331, T329)
U8_aag(T264, T265, T263, addcF_out_aag(T264, T265, T263)) → addzC_out_aag(one(T264), one(T265), zero(T263))
U29_aag(T250, T251, T249, addzC_out_aag(T250, T251, T249)) → addyE_out_aag(T250, T251, T249)
U7_aag(T222, T223, T221, addyE_out_aag(T222, T223, T221)) → addzC_out_aag(one(T222), zero(T223), one(T221))
U26_aag(T202, T203, T201, addzC_out_aag(T202, T203, T201)) → addxD_out_aag(T202, T203, T201)
U6_aag(T174, T175, T173, addxD_out_aag(T174, T175, T173)) → addzC_out_aag(zero(T174), one(T175), one(T173))
U5_aag(T154, T155, T153, addzC_out_aag(T154, T155, T153)) → addzC_out_aag(zero(T154), zero(T155), zero(T153))
U30_aag(T134, T135, T133, addzC_out_aag(T134, T135, T133)) → addzJ_out_aag(zero(T134), zero(T135), zero(T133))
addzJ_in_aag(zero(T489), one(T490), one(T488)) → U31_aag(T489, T490, T488, addxD_in_aag(T489, T490, T488))
U31_aag(T489, T490, T488, addxD_out_aag(T489, T490, T488)) → addzJ_out_aag(zero(T489), one(T490), one(T488))
addzJ_in_aag(one(T507), zero(T508), one(T506)) → U32_aag(T507, T508, T506, addyE_in_aag(T507, T508, T506))
U32_aag(T507, T508, T506, addyE_out_aag(T507, T508, T506)) → addzJ_out_aag(one(T507), zero(T508), one(T506))
addzJ_in_aag(one(T519), one(T520), zero(T518)) → U33_aag(T519, T520, T518, addcF_in_aag(T519, T520, T518))
U33_aag(T519, T520, T518, addcF_out_aag(T519, T520, T518)) → addzJ_out_aag(one(T519), one(T520), zero(T518))
U37_aag(T114, T115, T113, addzJ_out_aag(T114, T115, T113)) → addK_out_aag(T114, T115, T113)
addK_in_aag(b, zero(T527), zero(T527)) → U38_aag(T527, binaryZA_in_g(T527))
U38_aag(T527, binaryZA_out_g(T527)) → addK_out_aag(b, zero(T527), zero(T527))
addK_in_aag(b, one(T533), one(T533)) → U39_aag(T533, binaryB_in_g(T533))
U39_aag(T533, binaryB_out_g(T533)) → addK_out_aag(b, one(T533), one(T533))
addK_in_aag(T548, T549, T547) → U40_aag(T548, T549, T547, addzJ_in_aag(T548, T549, T547))
U40_aag(T548, T549, T547, addzJ_out_aag(T548, T549, T547)) → addK_out_aag(T548, T549, T547)
addK_in_aag(zero(T576), zero(T577), zero(T575)) → U41_aag(T576, T577, T575, addzC_in_aag(T576, T577, T575))
U41_aag(T576, T577, T575, addzC_out_aag(T576, T577, T575)) → addK_out_aag(zero(T576), zero(T577), zero(T575))
addK_in_aag(zero(T596), one(T597), one(T595)) → U42_aag(T596, T597, T595, addxD_in_aag(T596, T597, T595))
U42_aag(T596, T597, T595, addxD_out_aag(T596, T597, T595)) → addK_out_aag(zero(T596), one(T597), one(T595))
addK_in_aag(one(T614), zero(T615), one(T613)) → U43_aag(T614, T615, T613, addyE_in_aag(T614, T615, T613))
U43_aag(T614, T615, T613, addyE_out_aag(T614, T615, T613)) → addK_out_aag(one(T614), zero(T615), one(T613))
addK_in_aag(one(T626), one(T627), zero(T625)) → U44_aag(T626, T627, T625, addcF_in_aag(T626, T627, T625))
U44_aag(T626, T627, T625, addcF_out_aag(T626, T627, T625)) → addK_out_aag(one(T626), one(T627), zero(T625))
BINARYZA_IN_G(one(T79)) → BINARYB_IN_G(T79)
BINARYB_IN_G(zero(T84)) → BINARYZA_IN_G(T84)
BINARYZA_IN_G(zero(T75)) → BINARYZA_IN_G(T75)
BINARYB_IN_G(one(T88)) → BINARYB_IN_G(T88)
addK_in_aag(b, b, b) → addK_out_aag(b, b, b)
addK_in_aag(zero(T69), b, zero(T69)) → U34_aag(T69, binaryZA_in_g(T69))
binaryZA_in_g(zero(T75)) → U1_g(T75, binaryZA_in_g(T75))
binaryZA_in_g(one(T79)) → U2_g(T79, binaryB_in_g(T79))
binaryB_in_g(b) → binaryB_out_g(b)
binaryB_in_g(zero(T84)) → U3_g(T84, binaryZA_in_g(T84))
U3_g(T84, binaryZA_out_g(T84)) → binaryB_out_g(zero(T84))
binaryB_in_g(one(T88)) → U4_g(T88, binaryB_in_g(T88))
U4_g(T88, binaryB_out_g(T88)) → binaryB_out_g(one(T88))
U2_g(T79, binaryB_out_g(T79)) → binaryZA_out_g(one(T79))
U1_g(T75, binaryZA_out_g(T75)) → binaryZA_out_g(zero(T75))
U34_aag(T69, binaryZA_out_g(T69)) → addK_out_aag(zero(T69), b, zero(T69))
addK_in_aag(one(T93), b, one(T93)) → U35_aag(T93, binaryB_in_g(T93))
U35_aag(T93, binaryB_out_g(T93)) → addK_out_aag(one(T93), b, one(T93))
addK_in_aag(b, T98, T98) → U36_aag(T98, binaryZA_in_g(T98))
U36_aag(T98, binaryZA_out_g(T98)) → addK_out_aag(b, T98, T98)
addK_in_aag(T114, T115, T113) → U37_aag(T114, T115, T113, addzJ_in_aag(T114, T115, T113))
addzJ_in_aag(zero(T134), zero(T135), zero(T133)) → U30_aag(T134, T135, T133, addzC_in_aag(T134, T135, T133))
addzC_in_aag(zero(T154), zero(T155), zero(T153)) → U5_aag(T154, T155, T153, addzC_in_aag(T154, T155, T153))
addzC_in_aag(zero(T174), one(T175), one(T173)) → U6_aag(T174, T175, T173, addxD_in_aag(T174, T175, T173))
addxD_in_aag(one(T181), b, one(T181)) → U24_aag(T181, binaryB_in_g(T181))
U24_aag(T181, binaryB_out_g(T181)) → addxD_out_aag(one(T181), b, one(T181))
addxD_in_aag(zero(T186), b, zero(T186)) → U25_aag(T186, binaryZA_in_g(T186))
U25_aag(T186, binaryZA_out_g(T186)) → addxD_out_aag(zero(T186), b, zero(T186))
addxD_in_aag(T202, T203, T201) → U26_aag(T202, T203, T201, addzC_in_aag(T202, T203, T201))
addzC_in_aag(one(T222), zero(T223), one(T221)) → U7_aag(T222, T223, T221, addyE_in_aag(T222, T223, T221))
addyE_in_aag(b, one(T229), one(T229)) → U27_aag(T229, binaryB_in_g(T229))
U27_aag(T229, binaryB_out_g(T229)) → addyE_out_aag(b, one(T229), one(T229))
addyE_in_aag(b, zero(T234), zero(T234)) → U28_aag(T234, binaryZA_in_g(T234))
U28_aag(T234, binaryZA_out_g(T234)) → addyE_out_aag(b, zero(T234), zero(T234))
addyE_in_aag(T250, T251, T249) → U29_aag(T250, T251, T249, addzC_in_aag(T250, T251, T249))
addzC_in_aag(one(T264), one(T265), zero(T263)) → U8_aag(T264, T265, T263, addcF_in_aag(T264, T265, T263))
addcF_in_aag(b, b, one(b)) → addcF_out_aag(b, b, one(b))
addcF_in_aag(T276, b, T275) → U21_aag(T276, T275, succZH_in_ag(T276, T275))
succZH_in_ag(zero(T282), one(T282)) → U11_ag(T282, binaryZA_in_g(T282))
U11_ag(T282, binaryZA_out_g(T282)) → succZH_out_ag(zero(T282), one(T282))
succZH_in_ag(one(T290), zero(T289)) → U12_ag(T290, T289, succG_in_ag(T290, T289))
succG_in_ag(b, one(b)) → succG_out_ag(b, one(b))
succG_in_ag(zero(T295), one(T295)) → U9_ag(T295, binaryZA_in_g(T295))
U9_ag(T295, binaryZA_out_g(T295)) → succG_out_ag(zero(T295), one(T295))
succG_in_ag(one(T303), zero(T302)) → U10_ag(T303, T302, succG_in_ag(T303, T302))
U10_ag(T303, T302, succG_out_ag(T303, T302)) → succG_out_ag(one(T303), zero(T302))
U12_ag(T290, T289, succG_out_ag(T290, T289)) → succZH_out_ag(one(T290), zero(T289))
U21_aag(T276, T275, succZH_out_ag(T276, T275)) → addcF_out_aag(T276, b, T275)
addcF_in_aag(b, T314, T313) → U22_aag(T314, T313, succZH_in_ag(T314, T313))
U22_aag(T314, T313, succZH_out_ag(T314, T313)) → addcF_out_aag(b, T314, T313)
addcF_in_aag(T330, T331, T329) → U23_aag(T330, T331, T329, addCI_in_aag(T330, T331, T329))
addCI_in_aag(zero(T350), zero(T351), one(T349)) → U13_aag(T350, T351, T349, addzC_in_aag(T350, T351, T349))
U13_aag(T350, T351, T349, addzC_out_aag(T350, T351, T349)) → addCI_out_aag(zero(T350), zero(T351), one(T349))
addCI_in_aag(zero(zero(T377)), one(b), zero(one(T377))) → U14_aag(T377, binaryZA_in_g(T377))
U14_aag(T377, binaryZA_out_g(T377)) → addCI_out_aag(zero(zero(T377)), one(b), zero(one(T377)))
addCI_in_aag(zero(one(T389)), one(b), zero(zero(T388))) → U15_aag(T389, T388, succG_in_ag(T389, T388))
U15_aag(T389, T388, succG_out_ag(T389, T388)) → addCI_out_aag(zero(one(T389)), one(b), zero(zero(T388)))
addCI_in_aag(zero(T404), one(T405), zero(T403)) → U16_aag(T404, T405, T403, addCI_in_aag(T404, T405, T403))
addCI_in_aag(one(b), zero(zero(T431)), zero(one(T431))) → U17_aag(T431, binaryZA_in_g(T431))
U17_aag(T431, binaryZA_out_g(T431)) → addCI_out_aag(one(b), zero(zero(T431)), zero(one(T431)))
addCI_in_aag(one(b), zero(one(T443)), zero(zero(T442))) → U18_aag(T443, T442, succG_in_ag(T443, T442))
U18_aag(T443, T442, succG_out_ag(T443, T442)) → addCI_out_aag(one(b), zero(one(T443)), zero(zero(T442)))
addCI_in_aag(one(T458), zero(T459), zero(T457)) → U19_aag(T458, T459, T457, addCI_in_aag(T458, T459, T457))
addCI_in_aag(one(T472), one(T473), one(T471)) → U20_aag(T472, T473, T471, addcF_in_aag(T472, T473, T471))
U20_aag(T472, T473, T471, addcF_out_aag(T472, T473, T471)) → addCI_out_aag(one(T472), one(T473), one(T471))
U19_aag(T458, T459, T457, addCI_out_aag(T458, T459, T457)) → addCI_out_aag(one(T458), zero(T459), zero(T457))
U16_aag(T404, T405, T403, addCI_out_aag(T404, T405, T403)) → addCI_out_aag(zero(T404), one(T405), zero(T403))
U23_aag(T330, T331, T329, addCI_out_aag(T330, T331, T329)) → addcF_out_aag(T330, T331, T329)
U8_aag(T264, T265, T263, addcF_out_aag(T264, T265, T263)) → addzC_out_aag(one(T264), one(T265), zero(T263))
U29_aag(T250, T251, T249, addzC_out_aag(T250, T251, T249)) → addyE_out_aag(T250, T251, T249)
U7_aag(T222, T223, T221, addyE_out_aag(T222, T223, T221)) → addzC_out_aag(one(T222), zero(T223), one(T221))
U26_aag(T202, T203, T201, addzC_out_aag(T202, T203, T201)) → addxD_out_aag(T202, T203, T201)
U6_aag(T174, T175, T173, addxD_out_aag(T174, T175, T173)) → addzC_out_aag(zero(T174), one(T175), one(T173))
U5_aag(T154, T155, T153, addzC_out_aag(T154, T155, T153)) → addzC_out_aag(zero(T154), zero(T155), zero(T153))
U30_aag(T134, T135, T133, addzC_out_aag(T134, T135, T133)) → addzJ_out_aag(zero(T134), zero(T135), zero(T133))
addzJ_in_aag(zero(T489), one(T490), one(T488)) → U31_aag(T489, T490, T488, addxD_in_aag(T489, T490, T488))
U31_aag(T489, T490, T488, addxD_out_aag(T489, T490, T488)) → addzJ_out_aag(zero(T489), one(T490), one(T488))
addzJ_in_aag(one(T507), zero(T508), one(T506)) → U32_aag(T507, T508, T506, addyE_in_aag(T507, T508, T506))
U32_aag(T507, T508, T506, addyE_out_aag(T507, T508, T506)) → addzJ_out_aag(one(T507), zero(T508), one(T506))
addzJ_in_aag(one(T519), one(T520), zero(T518)) → U33_aag(T519, T520, T518, addcF_in_aag(T519, T520, T518))
U33_aag(T519, T520, T518, addcF_out_aag(T519, T520, T518)) → addzJ_out_aag(one(T519), one(T520), zero(T518))
U37_aag(T114, T115, T113, addzJ_out_aag(T114, T115, T113)) → addK_out_aag(T114, T115, T113)
addK_in_aag(b, zero(T527), zero(T527)) → U38_aag(T527, binaryZA_in_g(T527))
U38_aag(T527, binaryZA_out_g(T527)) → addK_out_aag(b, zero(T527), zero(T527))
addK_in_aag(b, one(T533), one(T533)) → U39_aag(T533, binaryB_in_g(T533))
U39_aag(T533, binaryB_out_g(T533)) → addK_out_aag(b, one(T533), one(T533))
addK_in_aag(T548, T549, T547) → U40_aag(T548, T549, T547, addzJ_in_aag(T548, T549, T547))
U40_aag(T548, T549, T547, addzJ_out_aag(T548, T549, T547)) → addK_out_aag(T548, T549, T547)
addK_in_aag(zero(T576), zero(T577), zero(T575)) → U41_aag(T576, T577, T575, addzC_in_aag(T576, T577, T575))
U41_aag(T576, T577, T575, addzC_out_aag(T576, T577, T575)) → addK_out_aag(zero(T576), zero(T577), zero(T575))
addK_in_aag(zero(T596), one(T597), one(T595)) → U42_aag(T596, T597, T595, addxD_in_aag(T596, T597, T595))
U42_aag(T596, T597, T595, addxD_out_aag(T596, T597, T595)) → addK_out_aag(zero(T596), one(T597), one(T595))
addK_in_aag(one(T614), zero(T615), one(T613)) → U43_aag(T614, T615, T613, addyE_in_aag(T614, T615, T613))
U43_aag(T614, T615, T613, addyE_out_aag(T614, T615, T613)) → addK_out_aag(one(T614), zero(T615), one(T613))
addK_in_aag(one(T626), one(T627), zero(T625)) → U44_aag(T626, T627, T625, addcF_in_aag(T626, T627, T625))
U44_aag(T626, T627, T625, addcF_out_aag(T626, T627, T625)) → addK_out_aag(one(T626), one(T627), zero(T625))
BINARYZA_IN_G(one(T79)) → BINARYB_IN_G(T79)
BINARYB_IN_G(zero(T84)) → BINARYZA_IN_G(T84)
BINARYZA_IN_G(zero(T75)) → BINARYZA_IN_G(T75)
BINARYB_IN_G(one(T88)) → BINARYB_IN_G(T88)
BINARYZA_IN_G(one(T79)) → BINARYB_IN_G(T79)
BINARYB_IN_G(zero(T84)) → BINARYZA_IN_G(T84)
BINARYZA_IN_G(zero(T75)) → BINARYZA_IN_G(T75)
BINARYB_IN_G(one(T88)) → BINARYB_IN_G(T88)
From the DPs we obtained the following set of size-change graphs:
SUCCG_IN_AG(one(T303), zero(T302)) → SUCCG_IN_AG(T303, T302)
addK_in_aag(b, b, b) → addK_out_aag(b, b, b)
addK_in_aag(zero(T69), b, zero(T69)) → U34_aag(T69, binaryZA_in_g(T69))
binaryZA_in_g(zero(T75)) → U1_g(T75, binaryZA_in_g(T75))
binaryZA_in_g(one(T79)) → U2_g(T79, binaryB_in_g(T79))
binaryB_in_g(b) → binaryB_out_g(b)
binaryB_in_g(zero(T84)) → U3_g(T84, binaryZA_in_g(T84))
U3_g(T84, binaryZA_out_g(T84)) → binaryB_out_g(zero(T84))
binaryB_in_g(one(T88)) → U4_g(T88, binaryB_in_g(T88))
U4_g(T88, binaryB_out_g(T88)) → binaryB_out_g(one(T88))
U2_g(T79, binaryB_out_g(T79)) → binaryZA_out_g(one(T79))
U1_g(T75, binaryZA_out_g(T75)) → binaryZA_out_g(zero(T75))
U34_aag(T69, binaryZA_out_g(T69)) → addK_out_aag(zero(T69), b, zero(T69))
addK_in_aag(one(T93), b, one(T93)) → U35_aag(T93, binaryB_in_g(T93))
U35_aag(T93, binaryB_out_g(T93)) → addK_out_aag(one(T93), b, one(T93))
addK_in_aag(b, T98, T98) → U36_aag(T98, binaryZA_in_g(T98))
U36_aag(T98, binaryZA_out_g(T98)) → addK_out_aag(b, T98, T98)
addK_in_aag(T114, T115, T113) → U37_aag(T114, T115, T113, addzJ_in_aag(T114, T115, T113))
addzJ_in_aag(zero(T134), zero(T135), zero(T133)) → U30_aag(T134, T135, T133, addzC_in_aag(T134, T135, T133))
addzC_in_aag(zero(T154), zero(T155), zero(T153)) → U5_aag(T154, T155, T153, addzC_in_aag(T154, T155, T153))
addzC_in_aag(zero(T174), one(T175), one(T173)) → U6_aag(T174, T175, T173, addxD_in_aag(T174, T175, T173))
addxD_in_aag(one(T181), b, one(T181)) → U24_aag(T181, binaryB_in_g(T181))
U24_aag(T181, binaryB_out_g(T181)) → addxD_out_aag(one(T181), b, one(T181))
addxD_in_aag(zero(T186), b, zero(T186)) → U25_aag(T186, binaryZA_in_g(T186))
U25_aag(T186, binaryZA_out_g(T186)) → addxD_out_aag(zero(T186), b, zero(T186))
addxD_in_aag(T202, T203, T201) → U26_aag(T202, T203, T201, addzC_in_aag(T202, T203, T201))
addzC_in_aag(one(T222), zero(T223), one(T221)) → U7_aag(T222, T223, T221, addyE_in_aag(T222, T223, T221))
addyE_in_aag(b, one(T229), one(T229)) → U27_aag(T229, binaryB_in_g(T229))
U27_aag(T229, binaryB_out_g(T229)) → addyE_out_aag(b, one(T229), one(T229))
addyE_in_aag(b, zero(T234), zero(T234)) → U28_aag(T234, binaryZA_in_g(T234))
U28_aag(T234, binaryZA_out_g(T234)) → addyE_out_aag(b, zero(T234), zero(T234))
addyE_in_aag(T250, T251, T249) → U29_aag(T250, T251, T249, addzC_in_aag(T250, T251, T249))
addzC_in_aag(one(T264), one(T265), zero(T263)) → U8_aag(T264, T265, T263, addcF_in_aag(T264, T265, T263))
addcF_in_aag(b, b, one(b)) → addcF_out_aag(b, b, one(b))
addcF_in_aag(T276, b, T275) → U21_aag(T276, T275, succZH_in_ag(T276, T275))
succZH_in_ag(zero(T282), one(T282)) → U11_ag(T282, binaryZA_in_g(T282))
U11_ag(T282, binaryZA_out_g(T282)) → succZH_out_ag(zero(T282), one(T282))
succZH_in_ag(one(T290), zero(T289)) → U12_ag(T290, T289, succG_in_ag(T290, T289))
succG_in_ag(b, one(b)) → succG_out_ag(b, one(b))
succG_in_ag(zero(T295), one(T295)) → U9_ag(T295, binaryZA_in_g(T295))
U9_ag(T295, binaryZA_out_g(T295)) → succG_out_ag(zero(T295), one(T295))
succG_in_ag(one(T303), zero(T302)) → U10_ag(T303, T302, succG_in_ag(T303, T302))
U10_ag(T303, T302, succG_out_ag(T303, T302)) → succG_out_ag(one(T303), zero(T302))
U12_ag(T290, T289, succG_out_ag(T290, T289)) → succZH_out_ag(one(T290), zero(T289))
U21_aag(T276, T275, succZH_out_ag(T276, T275)) → addcF_out_aag(T276, b, T275)
addcF_in_aag(b, T314, T313) → U22_aag(T314, T313, succZH_in_ag(T314, T313))
U22_aag(T314, T313, succZH_out_ag(T314, T313)) → addcF_out_aag(b, T314, T313)
addcF_in_aag(T330, T331, T329) → U23_aag(T330, T331, T329, addCI_in_aag(T330, T331, T329))
addCI_in_aag(zero(T350), zero(T351), one(T349)) → U13_aag(T350, T351, T349, addzC_in_aag(T350, T351, T349))
U13_aag(T350, T351, T349, addzC_out_aag(T350, T351, T349)) → addCI_out_aag(zero(T350), zero(T351), one(T349))
addCI_in_aag(zero(zero(T377)), one(b), zero(one(T377))) → U14_aag(T377, binaryZA_in_g(T377))
U14_aag(T377, binaryZA_out_g(T377)) → addCI_out_aag(zero(zero(T377)), one(b), zero(one(T377)))
addCI_in_aag(zero(one(T389)), one(b), zero(zero(T388))) → U15_aag(T389, T388, succG_in_ag(T389, T388))
U15_aag(T389, T388, succG_out_ag(T389, T388)) → addCI_out_aag(zero(one(T389)), one(b), zero(zero(T388)))
addCI_in_aag(zero(T404), one(T405), zero(T403)) → U16_aag(T404, T405, T403, addCI_in_aag(T404, T405, T403))
addCI_in_aag(one(b), zero(zero(T431)), zero(one(T431))) → U17_aag(T431, binaryZA_in_g(T431))
U17_aag(T431, binaryZA_out_g(T431)) → addCI_out_aag(one(b), zero(zero(T431)), zero(one(T431)))
addCI_in_aag(one(b), zero(one(T443)), zero(zero(T442))) → U18_aag(T443, T442, succG_in_ag(T443, T442))
U18_aag(T443, T442, succG_out_ag(T443, T442)) → addCI_out_aag(one(b), zero(one(T443)), zero(zero(T442)))
addCI_in_aag(one(T458), zero(T459), zero(T457)) → U19_aag(T458, T459, T457, addCI_in_aag(T458, T459, T457))
addCI_in_aag(one(T472), one(T473), one(T471)) → U20_aag(T472, T473, T471, addcF_in_aag(T472, T473, T471))
U20_aag(T472, T473, T471, addcF_out_aag(T472, T473, T471)) → addCI_out_aag(one(T472), one(T473), one(T471))
U19_aag(T458, T459, T457, addCI_out_aag(T458, T459, T457)) → addCI_out_aag(one(T458), zero(T459), zero(T457))
U16_aag(T404, T405, T403, addCI_out_aag(T404, T405, T403)) → addCI_out_aag(zero(T404), one(T405), zero(T403))
U23_aag(T330, T331, T329, addCI_out_aag(T330, T331, T329)) → addcF_out_aag(T330, T331, T329)
U8_aag(T264, T265, T263, addcF_out_aag(T264, T265, T263)) → addzC_out_aag(one(T264), one(T265), zero(T263))
U29_aag(T250, T251, T249, addzC_out_aag(T250, T251, T249)) → addyE_out_aag(T250, T251, T249)
U7_aag(T222, T223, T221, addyE_out_aag(T222, T223, T221)) → addzC_out_aag(one(T222), zero(T223), one(T221))
U26_aag(T202, T203, T201, addzC_out_aag(T202, T203, T201)) → addxD_out_aag(T202, T203, T201)
U6_aag(T174, T175, T173, addxD_out_aag(T174, T175, T173)) → addzC_out_aag(zero(T174), one(T175), one(T173))
U5_aag(T154, T155, T153, addzC_out_aag(T154, T155, T153)) → addzC_out_aag(zero(T154), zero(T155), zero(T153))
U30_aag(T134, T135, T133, addzC_out_aag(T134, T135, T133)) → addzJ_out_aag(zero(T134), zero(T135), zero(T133))
addzJ_in_aag(zero(T489), one(T490), one(T488)) → U31_aag(T489, T490, T488, addxD_in_aag(T489, T490, T488))
U31_aag(T489, T490, T488, addxD_out_aag(T489, T490, T488)) → addzJ_out_aag(zero(T489), one(T490), one(T488))
addzJ_in_aag(one(T507), zero(T508), one(T506)) → U32_aag(T507, T508, T506, addyE_in_aag(T507, T508, T506))
U32_aag(T507, T508, T506, addyE_out_aag(T507, T508, T506)) → addzJ_out_aag(one(T507), zero(T508), one(T506))
addzJ_in_aag(one(T519), one(T520), zero(T518)) → U33_aag(T519, T520, T518, addcF_in_aag(T519, T520, T518))
U33_aag(T519, T520, T518, addcF_out_aag(T519, T520, T518)) → addzJ_out_aag(one(T519), one(T520), zero(T518))
U37_aag(T114, T115, T113, addzJ_out_aag(T114, T115, T113)) → addK_out_aag(T114, T115, T113)
addK_in_aag(b, zero(T527), zero(T527)) → U38_aag(T527, binaryZA_in_g(T527))
U38_aag(T527, binaryZA_out_g(T527)) → addK_out_aag(b, zero(T527), zero(T527))
addK_in_aag(b, one(T533), one(T533)) → U39_aag(T533, binaryB_in_g(T533))
U39_aag(T533, binaryB_out_g(T533)) → addK_out_aag(b, one(T533), one(T533))
addK_in_aag(T548, T549, T547) → U40_aag(T548, T549, T547, addzJ_in_aag(T548, T549, T547))
U40_aag(T548, T549, T547, addzJ_out_aag(T548, T549, T547)) → addK_out_aag(T548, T549, T547)
addK_in_aag(zero(T576), zero(T577), zero(T575)) → U41_aag(T576, T577, T575, addzC_in_aag(T576, T577, T575))
U41_aag(T576, T577, T575, addzC_out_aag(T576, T577, T575)) → addK_out_aag(zero(T576), zero(T577), zero(T575))
addK_in_aag(zero(T596), one(T597), one(T595)) → U42_aag(T596, T597, T595, addxD_in_aag(T596, T597, T595))
U42_aag(T596, T597, T595, addxD_out_aag(T596, T597, T595)) → addK_out_aag(zero(T596), one(T597), one(T595))
addK_in_aag(one(T614), zero(T615), one(T613)) → U43_aag(T614, T615, T613, addyE_in_aag(T614, T615, T613))
U43_aag(T614, T615, T613, addyE_out_aag(T614, T615, T613)) → addK_out_aag(one(T614), zero(T615), one(T613))
addK_in_aag(one(T626), one(T627), zero(T625)) → U44_aag(T626, T627, T625, addcF_in_aag(T626, T627, T625))
U44_aag(T626, T627, T625, addcF_out_aag(T626, T627, T625)) → addK_out_aag(one(T626), one(T627), zero(T625))
SUCCG_IN_AG(one(T303), zero(T302)) → SUCCG_IN_AG(T303, T302)
SUCCG_IN_AG(zero(T302)) → SUCCG_IN_AG(T302)
From the DPs we obtained the following set of size-change graphs:
ADDXD_IN_AAG(T202, T203, T201) → ADDZC_IN_AAG(T202, T203, T201)
ADDZC_IN_AAG(zero(T154), zero(T155), zero(T153)) → ADDZC_IN_AAG(T154, T155, T153)
ADDZC_IN_AAG(zero(T174), one(T175), one(T173)) → ADDXD_IN_AAG(T174, T175, T173)
ADDZC_IN_AAG(one(T222), zero(T223), one(T221)) → ADDYE_IN_AAG(T222, T223, T221)
ADDYE_IN_AAG(T250, T251, T249) → ADDZC_IN_AAG(T250, T251, T249)
ADDZC_IN_AAG(one(T264), one(T265), zero(T263)) → ADDCF_IN_AAG(T264, T265, T263)
ADDCF_IN_AAG(T330, T331, T329) → ADDCI_IN_AAG(T330, T331, T329)
ADDCI_IN_AAG(zero(T350), zero(T351), one(T349)) → ADDZC_IN_AAG(T350, T351, T349)
ADDCI_IN_AAG(zero(T404), one(T405), zero(T403)) → ADDCI_IN_AAG(T404, T405, T403)
ADDCI_IN_AAG(one(T458), zero(T459), zero(T457)) → ADDCI_IN_AAG(T458, T459, T457)
ADDCI_IN_AAG(one(T472), one(T473), one(T471)) → ADDCF_IN_AAG(T472, T473, T471)
addK_in_aag(b, b, b) → addK_out_aag(b, b, b)
addK_in_aag(zero(T69), b, zero(T69)) → U34_aag(T69, binaryZA_in_g(T69))
binaryZA_in_g(zero(T75)) → U1_g(T75, binaryZA_in_g(T75))
binaryZA_in_g(one(T79)) → U2_g(T79, binaryB_in_g(T79))
binaryB_in_g(b) → binaryB_out_g(b)
binaryB_in_g(zero(T84)) → U3_g(T84, binaryZA_in_g(T84))
U3_g(T84, binaryZA_out_g(T84)) → binaryB_out_g(zero(T84))
binaryB_in_g(one(T88)) → U4_g(T88, binaryB_in_g(T88))
U4_g(T88, binaryB_out_g(T88)) → binaryB_out_g(one(T88))
U2_g(T79, binaryB_out_g(T79)) → binaryZA_out_g(one(T79))
U1_g(T75, binaryZA_out_g(T75)) → binaryZA_out_g(zero(T75))
U34_aag(T69, binaryZA_out_g(T69)) → addK_out_aag(zero(T69), b, zero(T69))
addK_in_aag(one(T93), b, one(T93)) → U35_aag(T93, binaryB_in_g(T93))
U35_aag(T93, binaryB_out_g(T93)) → addK_out_aag(one(T93), b, one(T93))
addK_in_aag(b, T98, T98) → U36_aag(T98, binaryZA_in_g(T98))
U36_aag(T98, binaryZA_out_g(T98)) → addK_out_aag(b, T98, T98)
addK_in_aag(T114, T115, T113) → U37_aag(T114, T115, T113, addzJ_in_aag(T114, T115, T113))
addzJ_in_aag(zero(T134), zero(T135), zero(T133)) → U30_aag(T134, T135, T133, addzC_in_aag(T134, T135, T133))
addzC_in_aag(zero(T154), zero(T155), zero(T153)) → U5_aag(T154, T155, T153, addzC_in_aag(T154, T155, T153))
addzC_in_aag(zero(T174), one(T175), one(T173)) → U6_aag(T174, T175, T173, addxD_in_aag(T174, T175, T173))
addxD_in_aag(one(T181), b, one(T181)) → U24_aag(T181, binaryB_in_g(T181))
U24_aag(T181, binaryB_out_g(T181)) → addxD_out_aag(one(T181), b, one(T181))
addxD_in_aag(zero(T186), b, zero(T186)) → U25_aag(T186, binaryZA_in_g(T186))
U25_aag(T186, binaryZA_out_g(T186)) → addxD_out_aag(zero(T186), b, zero(T186))
addxD_in_aag(T202, T203, T201) → U26_aag(T202, T203, T201, addzC_in_aag(T202, T203, T201))
addzC_in_aag(one(T222), zero(T223), one(T221)) → U7_aag(T222, T223, T221, addyE_in_aag(T222, T223, T221))
addyE_in_aag(b, one(T229), one(T229)) → U27_aag(T229, binaryB_in_g(T229))
U27_aag(T229, binaryB_out_g(T229)) → addyE_out_aag(b, one(T229), one(T229))
addyE_in_aag(b, zero(T234), zero(T234)) → U28_aag(T234, binaryZA_in_g(T234))
U28_aag(T234, binaryZA_out_g(T234)) → addyE_out_aag(b, zero(T234), zero(T234))
addyE_in_aag(T250, T251, T249) → U29_aag(T250, T251, T249, addzC_in_aag(T250, T251, T249))
addzC_in_aag(one(T264), one(T265), zero(T263)) → U8_aag(T264, T265, T263, addcF_in_aag(T264, T265, T263))
addcF_in_aag(b, b, one(b)) → addcF_out_aag(b, b, one(b))
addcF_in_aag(T276, b, T275) → U21_aag(T276, T275, succZH_in_ag(T276, T275))
succZH_in_ag(zero(T282), one(T282)) → U11_ag(T282, binaryZA_in_g(T282))
U11_ag(T282, binaryZA_out_g(T282)) → succZH_out_ag(zero(T282), one(T282))
succZH_in_ag(one(T290), zero(T289)) → U12_ag(T290, T289, succG_in_ag(T290, T289))
succG_in_ag(b, one(b)) → succG_out_ag(b, one(b))
succG_in_ag(zero(T295), one(T295)) → U9_ag(T295, binaryZA_in_g(T295))
U9_ag(T295, binaryZA_out_g(T295)) → succG_out_ag(zero(T295), one(T295))
succG_in_ag(one(T303), zero(T302)) → U10_ag(T303, T302, succG_in_ag(T303, T302))
U10_ag(T303, T302, succG_out_ag(T303, T302)) → succG_out_ag(one(T303), zero(T302))
U12_ag(T290, T289, succG_out_ag(T290, T289)) → succZH_out_ag(one(T290), zero(T289))
U21_aag(T276, T275, succZH_out_ag(T276, T275)) → addcF_out_aag(T276, b, T275)
addcF_in_aag(b, T314, T313) → U22_aag(T314, T313, succZH_in_ag(T314, T313))
U22_aag(T314, T313, succZH_out_ag(T314, T313)) → addcF_out_aag(b, T314, T313)
addcF_in_aag(T330, T331, T329) → U23_aag(T330, T331, T329, addCI_in_aag(T330, T331, T329))
addCI_in_aag(zero(T350), zero(T351), one(T349)) → U13_aag(T350, T351, T349, addzC_in_aag(T350, T351, T349))
U13_aag(T350, T351, T349, addzC_out_aag(T350, T351, T349)) → addCI_out_aag(zero(T350), zero(T351), one(T349))
addCI_in_aag(zero(zero(T377)), one(b), zero(one(T377))) → U14_aag(T377, binaryZA_in_g(T377))
U14_aag(T377, binaryZA_out_g(T377)) → addCI_out_aag(zero(zero(T377)), one(b), zero(one(T377)))
addCI_in_aag(zero(one(T389)), one(b), zero(zero(T388))) → U15_aag(T389, T388, succG_in_ag(T389, T388))
U15_aag(T389, T388, succG_out_ag(T389, T388)) → addCI_out_aag(zero(one(T389)), one(b), zero(zero(T388)))
addCI_in_aag(zero(T404), one(T405), zero(T403)) → U16_aag(T404, T405, T403, addCI_in_aag(T404, T405, T403))
addCI_in_aag(one(b), zero(zero(T431)), zero(one(T431))) → U17_aag(T431, binaryZA_in_g(T431))
U17_aag(T431, binaryZA_out_g(T431)) → addCI_out_aag(one(b), zero(zero(T431)), zero(one(T431)))
addCI_in_aag(one(b), zero(one(T443)), zero(zero(T442))) → U18_aag(T443, T442, succG_in_ag(T443, T442))
U18_aag(T443, T442, succG_out_ag(T443, T442)) → addCI_out_aag(one(b), zero(one(T443)), zero(zero(T442)))
addCI_in_aag(one(T458), zero(T459), zero(T457)) → U19_aag(T458, T459, T457, addCI_in_aag(T458, T459, T457))
addCI_in_aag(one(T472), one(T473), one(T471)) → U20_aag(T472, T473, T471, addcF_in_aag(T472, T473, T471))
U20_aag(T472, T473, T471, addcF_out_aag(T472, T473, T471)) → addCI_out_aag(one(T472), one(T473), one(T471))
U19_aag(T458, T459, T457, addCI_out_aag(T458, T459, T457)) → addCI_out_aag(one(T458), zero(T459), zero(T457))
U16_aag(T404, T405, T403, addCI_out_aag(T404, T405, T403)) → addCI_out_aag(zero(T404), one(T405), zero(T403))
U23_aag(T330, T331, T329, addCI_out_aag(T330, T331, T329)) → addcF_out_aag(T330, T331, T329)
U8_aag(T264, T265, T263, addcF_out_aag(T264, T265, T263)) → addzC_out_aag(one(T264), one(T265), zero(T263))
U29_aag(T250, T251, T249, addzC_out_aag(T250, T251, T249)) → addyE_out_aag(T250, T251, T249)
U7_aag(T222, T223, T221, addyE_out_aag(T222, T223, T221)) → addzC_out_aag(one(T222), zero(T223), one(T221))
U26_aag(T202, T203, T201, addzC_out_aag(T202, T203, T201)) → addxD_out_aag(T202, T203, T201)
U6_aag(T174, T175, T173, addxD_out_aag(T174, T175, T173)) → addzC_out_aag(zero(T174), one(T175), one(T173))
U5_aag(T154, T155, T153, addzC_out_aag(T154, T155, T153)) → addzC_out_aag(zero(T154), zero(T155), zero(T153))
U30_aag(T134, T135, T133, addzC_out_aag(T134, T135, T133)) → addzJ_out_aag(zero(T134), zero(T135), zero(T133))
addzJ_in_aag(zero(T489), one(T490), one(T488)) → U31_aag(T489, T490, T488, addxD_in_aag(T489, T490, T488))
U31_aag(T489, T490, T488, addxD_out_aag(T489, T490, T488)) → addzJ_out_aag(zero(T489), one(T490), one(T488))
addzJ_in_aag(one(T507), zero(T508), one(T506)) → U32_aag(T507, T508, T506, addyE_in_aag(T507, T508, T506))
U32_aag(T507, T508, T506, addyE_out_aag(T507, T508, T506)) → addzJ_out_aag(one(T507), zero(T508), one(T506))
addzJ_in_aag(one(T519), one(T520), zero(T518)) → U33_aag(T519, T520, T518, addcF_in_aag(T519, T520, T518))
U33_aag(T519, T520, T518, addcF_out_aag(T519, T520, T518)) → addzJ_out_aag(one(T519), one(T520), zero(T518))
U37_aag(T114, T115, T113, addzJ_out_aag(T114, T115, T113)) → addK_out_aag(T114, T115, T113)
addK_in_aag(b, zero(T527), zero(T527)) → U38_aag(T527, binaryZA_in_g(T527))
U38_aag(T527, binaryZA_out_g(T527)) → addK_out_aag(b, zero(T527), zero(T527))
addK_in_aag(b, one(T533), one(T533)) → U39_aag(T533, binaryB_in_g(T533))
U39_aag(T533, binaryB_out_g(T533)) → addK_out_aag(b, one(T533), one(T533))
addK_in_aag(T548, T549, T547) → U40_aag(T548, T549, T547, addzJ_in_aag(T548, T549, T547))
U40_aag(T548, T549, T547, addzJ_out_aag(T548, T549, T547)) → addK_out_aag(T548, T549, T547)
addK_in_aag(zero(T576), zero(T577), zero(T575)) → U41_aag(T576, T577, T575, addzC_in_aag(T576, T577, T575))
U41_aag(T576, T577, T575, addzC_out_aag(T576, T577, T575)) → addK_out_aag(zero(T576), zero(T577), zero(T575))
addK_in_aag(zero(T596), one(T597), one(T595)) → U42_aag(T596, T597, T595, addxD_in_aag(T596, T597, T595))
U42_aag(T596, T597, T595, addxD_out_aag(T596, T597, T595)) → addK_out_aag(zero(T596), one(T597), one(T595))
addK_in_aag(one(T614), zero(T615), one(T613)) → U43_aag(T614, T615, T613, addyE_in_aag(T614, T615, T613))
U43_aag(T614, T615, T613, addyE_out_aag(T614, T615, T613)) → addK_out_aag(one(T614), zero(T615), one(T613))
addK_in_aag(one(T626), one(T627), zero(T625)) → U44_aag(T626, T627, T625, addcF_in_aag(T626, T627, T625))
U44_aag(T626, T627, T625, addcF_out_aag(T626, T627, T625)) → addK_out_aag(one(T626), one(T627), zero(T625))
ADDXD_IN_AAG(T202, T203, T201) → ADDZC_IN_AAG(T202, T203, T201)
ADDZC_IN_AAG(zero(T154), zero(T155), zero(T153)) → ADDZC_IN_AAG(T154, T155, T153)
ADDZC_IN_AAG(zero(T174), one(T175), one(T173)) → ADDXD_IN_AAG(T174, T175, T173)
ADDZC_IN_AAG(one(T222), zero(T223), one(T221)) → ADDYE_IN_AAG(T222, T223, T221)
ADDYE_IN_AAG(T250, T251, T249) → ADDZC_IN_AAG(T250, T251, T249)
ADDZC_IN_AAG(one(T264), one(T265), zero(T263)) → ADDCF_IN_AAG(T264, T265, T263)
ADDCF_IN_AAG(T330, T331, T329) → ADDCI_IN_AAG(T330, T331, T329)
ADDCI_IN_AAG(zero(T350), zero(T351), one(T349)) → ADDZC_IN_AAG(T350, T351, T349)
ADDCI_IN_AAG(zero(T404), one(T405), zero(T403)) → ADDCI_IN_AAG(T404, T405, T403)
ADDCI_IN_AAG(one(T458), zero(T459), zero(T457)) → ADDCI_IN_AAG(T458, T459, T457)
ADDCI_IN_AAG(one(T472), one(T473), one(T471)) → ADDCF_IN_AAG(T472, T473, T471)
ADDXD_IN_AAG(T201) → ADDZC_IN_AAG(T201)
ADDZC_IN_AAG(zero(T153)) → ADDZC_IN_AAG(T153)
ADDZC_IN_AAG(one(T173)) → ADDXD_IN_AAG(T173)
ADDZC_IN_AAG(one(T221)) → ADDYE_IN_AAG(T221)
ADDYE_IN_AAG(T249) → ADDZC_IN_AAG(T249)
ADDZC_IN_AAG(zero(T263)) → ADDCF_IN_AAG(T263)
ADDCF_IN_AAG(T329) → ADDCI_IN_AAG(T329)
ADDCI_IN_AAG(one(T349)) → ADDZC_IN_AAG(T349)
ADDCI_IN_AAG(zero(T403)) → ADDCI_IN_AAG(T403)
ADDCI_IN_AAG(one(T471)) → ADDCF_IN_AAG(T471)
From the DPs we obtained the following set of size-change graphs: